perm filename CIRCUM.XGP[F83,JMC]7 blob sn#754699 filedate 1984-05-15 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ β∧Applications of Circumscription to Formalizing Common Sense Knowledge

␈↓ α∧␈↓α␈↓ ∧wby John McCarthy, Stanford University






␈↓ α∧␈↓Abstract:␈α
We␈α
present␈α
a␈α
new␈α
and␈α
more␈αsymmetric␈α
version␈α
of␈α
the␈α
circumscription␈α
method␈α
of␈αnon-
␈↓ α∧␈↓monotonic␈α∀reasoning␈α∃(McCarthy␈α∀1980)␈α∃and␈α∀some␈α∀applications␈α∃to␈α∀formalizing␈α∃common␈α∀sense
␈↓ α∧␈↓knowledge.␈α⊃ The␈α⊃applications␈α⊃in␈α⊃this␈α⊃paper␈α⊃are␈α⊃based␈α⊃on␈α⊃minimizing␈α⊃the␈α⊃abnormality␈α∩of␈α⊃the
␈↓ α∧␈↓different␈α∞aspects␈α∞of␈α
a␈α∞situation.␈α∞ Included␈α
are␈α∞non-monotonic␈α∞treatments␈α
of␈α∞␈↓↓is-a␈↓␈α∞hierarchies,␈α
the
␈↓ α∧␈↓unique names hypothesis, and the frame problem.






␈↓ α∧␈↓Descriptors: non-monotonic logic, common sense, artificial intelligence.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u2


␈↓ α∧␈↓1. ␈↓αIntroduction and new definition of circumscription␈↓

␈↓ α∧␈↓␈↓ αT(McCarthy␈α∂1980)␈α∞introduces␈α∂the␈α∞circumscription␈α∂method␈α∞of␈α∂non-monotonic␈α∂reasoning␈α∞and

␈↓ α∧␈↓gives␈αmotivation,␈αsome␈αmathematical␈αproperties␈αand␈αsome␈αexamples␈αof␈αits␈αapplication.␈α
 While␈αthe

␈↓ α∧␈↓present␈α⊃paper␈α⊃is␈α∩logically␈α⊃self-contained,␈α⊃motivation␈α⊃may␈α∩require␈α⊃some␈α⊃acquaintance␈α∩with␈α⊃the

␈↓ α∧␈↓earlier␈αpaper.␈α
 In␈αparticular␈α
we␈αdon't␈α
repeat␈αits␈α
arguments␈αabout␈α
the␈αimportance␈αof␈α
non-monotonic

␈↓ α∧␈↓reasoning in AI.  Also its examples are instructive.

␈↓ α∧␈↓␈↓ αTHere␈αwe␈αgive␈αa␈αmore␈αsymmetric␈α
definition␈αof␈αcircumscription␈αand␈αapplications␈αto␈αthe␈α
formal

␈↓ α∧␈↓expression␈α∂of␈α∂common␈α∂sense␈α∂facts.␈α∂ Our␈α∂goal␈α∂is␈α∂to␈α∂express␈α∂these␈α∂facts␈α∂in␈α∂a␈α∂way␈α∂that␈α∂would␈α∂be

␈↓ α∧␈↓suitable␈α∂for␈α⊂inclusion␈α∂in␈α∂a␈α⊂general␈α∂purpose␈α∂database␈α⊂of␈α∂common␈α∂sense␈α⊂facts.␈α∂ We␈α⊂imagine␈α∂this

␈↓ α∧␈↓database␈α
to␈α
be␈α
used␈α
by␈α
AI␈α
programs␈α
written␈α
after␈α
the␈α
initial␈α
preparation␈α
of␈α
the␈α
database.␈α
 It␈α
would

␈↓ α∧␈↓be␈α
best␈α
if␈α
the␈α
writers␈α∞of␈α
these␈α
programs␈α
didn't␈α
have␈α
to␈α∞be␈α
familiar␈α
with␈α
how␈α
the␈α∞common␈α
sense

␈↓ α∧␈↓facts␈α∃about␈α∀particular␈α∃phenomena␈α∃are␈α∀expressed.␈α∃ Thus␈α∃common␈α∀sense␈α∃knowledge␈α∃must␈α∀be

␈↓ α∧␈↓represented in a way that is not specific to a particular application.

␈↓ α∧␈↓␈↓ αTIt␈α∞turns␈α
out␈α∞that␈α
many␈α∞such␈α
common␈α∞sense␈α∞facts␈α
can␈α∞be␈α
formalized␈α∞in␈α
a␈α∞uniform␈α∞way.␈α
 A

␈↓ α∧␈↓single␈α∞predicate␈α∞␈↓↓ab,␈↓␈α∞standing␈α∞for␈α∞"abnormal"␈α∞is␈α∞circumscribed␈α∞with␈α∞certain␈α∞other␈α∞predicates␈α∞and

␈↓ α∧␈↓functions␈αconsidered␈αas␈α
variables␈αthat␈αcan␈α
be␈αconstrained␈αto␈α
achieve␈αthe␈αcircumscription␈αsubject␈α
to

␈↓ α∧␈↓the␈αaxioms.␈α So␈α
far␈αthis␈αseems␈αto␈α
cover␈αthe␈αuse␈αof␈α
circumscription␈αto␈αrepresent␈αdefault␈α
rules.␈α On

␈↓ α∧␈↓the␈αother␈αhand,␈αit␈αdoesn't␈αseem␈αthat␈αcircumscribing␈αabnormality␈αcan␈αbe␈αused␈αto␈αcover␈αmany␈αof␈αthe

␈↓ α∧␈↓examples␈α⊂of␈α⊂(McCarthy␈α⊂1980)␈α⊃in␈α⊂which␈α⊂we␈α⊂want␈α⊃to␈α⊂limit␈α⊂a␈α⊂set␈α⊃to␈α⊂those␈α⊂objects␈α⊂that␈α⊃must␈α⊂be

␈↓ α∧␈↓members.

␈↓ α∧␈↓2. A new version of circumscription.


␈↓ α∧␈↓␈↓αDefinition:␈↓␈αLet␈α
␈↓↓A(P)␈↓␈αbe␈αa␈α
formula␈αof␈αsecond␈α
order␈αlogic,␈α
where␈α␈↓↓P␈↓␈αis␈α
a␈αtuple␈αof␈α
some␈αof␈α
the␈αfree

␈↓ α∧␈↓predicate␈αsymbols␈αin␈α␈↓↓A(P).␈↓␈α
Let␈α␈↓↓E(P,x)␈↓␈αbe␈αa␈αwff␈α
in␈αwhich␈α␈↓↓P␈↓␈αand␈α
a␈αtuple␈α␈↓↓x␈↓␈αof␈αindividual␈α
variables

␈↓ α∧␈↓occur free.  The circumscription of ␈↓↓E(P,x)␈↓ relative to ␈↓↓A(P)␈↓ is the formula ␈↓↓A'(P)␈↓ defined by

␈↓ α∧␈↓1)␈↓ αt ␈↓↓A(P) ∧ ∀P'.[A(P') ∧ [∀x.E(P',x) ⊃ E(P,x)] ⊃ [∀x.E(P',x) ≡ E(P,x)]].␈↓
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u3


␈↓ α∧␈↓[We␈α⊃are␈α⊃here␈α⊃writing␈α⊃␈↓↓A(P)␈↓␈α⊃instead␈α⊂of␈α⊃␈↓↓A(P␈↓β1␈↓↓,...,P␈↓βn␈↓↓)␈↓␈α⊃for␈α⊃brevity␈α⊃and␈α⊃likewise␈α⊃writing␈α⊂␈↓↓E(P,x)␈↓

␈↓ α∧␈↓instead␈αof␈α␈↓↓E(P␈↓β1␈↓↓,...,P␈↓βn␈↓↓,x␈↓β1␈↓↓,...,x␈↓βn␈↓↓)␈↓.␈α Likewise␈αthe␈αquantifier␈α␈↓↓∀x␈↓␈αstands␈αfor␈α␈↓↓∀x␈↓β1␈↓↓...x␈↓βn␈↓↓␈↓.␈α In␈αprinciple

␈↓ α∧␈↓␈↓↓A(P)␈↓␈α∞may␈α∞have␈α∞embedded␈α∞quantifiers,␈α∞but␈α∞we␈α∞have␈α∞no␈α∞applications␈α∞yet␈α∞that␈α∞use␈α∞this␈α
generality.

␈↓ α∧␈↓Circumscription␈α
is␈α
a␈α
kind␈α
of␈αminimization,␈α
and␈α
the␈α
predicate␈α
symbols␈αin␈α
␈↓↓A(P)␈↓␈α
that␈α
are␈α
not␈α
in␈α␈↓↓P␈↓

␈↓ α∧␈↓itself act as parameters in this minimization.


␈↓ α∧␈↓␈↓ αTThere␈α
are␈αtwo␈α
differences␈α
between␈αthis␈α
and␈α(McCarthy␈α
1980).␈α
 First,␈αin␈α
that␈α
paper␈α␈↓↓E(P,x)␈↓

␈↓ α∧␈↓had␈αthe␈αspecific␈αform␈α␈↓↓P(x).␈↓␈α
Here␈αwe␈αspeak␈αof␈αcircumscribing␈αa␈α
wff,␈αwhile␈αthere␈αwe␈αcould␈αspeak␈α
of

␈↓ α∧␈↓circumscribing␈α
a␈α
predicate.␈α
 We␈α
can␈α
still␈α
speak␈α
of␈α
circumscribing␈α
the␈α
predicate␈α
␈↓↓P␈↓␈α
when␈α
␈↓↓E(P,x)␈↓␈α
has

␈↓ α∧␈↓the␈αspecial␈αform␈α␈↓↓P(x).␈↓␈αThe␈αpresent␈αform␈αis␈αmore␈αsymmetric␈αin␈αthat␈αall␈αof␈αthe␈αpredicate␈αsymbols␈αin

␈↓ α∧␈↓␈↓↓P␈↓␈α
are␈α
regarded␈α
as␈α
variables,␈αand␈α
a␈α
wff␈α
is␈α
minimized,␈αwhereas␈α
the␈α
earlier␈α
form␈α
distinguishes␈αone␈α
of

␈↓ α∧␈↓the␈αpredicates␈αthemselves␈αfor␈αminimization.␈α However,␈αthe␈αpresent␈αform␈αis␈αreducible␈αto␈αthe␈αearlier

␈↓ α∧␈↓form.

␈↓ α∧␈↓␈↓ αTSecond,␈α∩in␈α∩(1)␈α∩we␈α⊃use␈α∩an␈α∩explicit␈α∩quantifier␈α∩for␈α⊃the␈α∩predicate␈α∩variable␈α∩␈↓↓P'␈↓␈α∩whereas␈α⊃in

␈↓ α∧␈↓(McCarthy␈α
1980),␈α
the␈α
formula␈α
was␈α
a␈α
schema.␈α One␈α
advantage␈α
of␈α
the␈α
present␈α
formalism␈α
is␈αthat␈α
now

␈↓ α∧␈↓␈↓↓A'(P)␈↓␈α∀is␈α∃the␈α∀same␈α∀kind␈α∃of␈α∀formula␈α∃as␈α∀␈↓↓A(P)␈↓␈α∀and␈α∃can␈α∀be␈α∃used␈α∀as␈α∀part␈α∃of␈α∀the␈α∃axiom␈α∀for

␈↓ α∧␈↓circumscribing some other wff.

␈↓ α∧␈↓Remark:␈αThe␈αpredicate␈αsymbols␈α␈↓↓P␈↓β1␈↓↓,...,P␈↓βn␈↓↓␈↓␈αwill␈αnot␈αusually␈αbe␈αall␈αthe␈αpredicate␈αsymbols␈αoccurring

␈↓ α∧␈↓in␈α∀␈↓↓A(P).␈↓␈α∪The␈α∀situation␈α∪is␈α∀analogous␈α∀to␈α∪a␈α∀minimization␈α∪problem␈α∀in␈α∪calculus␈α∀or␈α∀calculus␈α∪of

␈↓ α∧␈↓variations.␈α
 Some␈α
quantity␈α
is␈αbeing␈α
minimized.␈α
 Other␈α
quantities␈αare␈α
variables␈α
whose␈α
values␈αare␈α
to

␈↓ α∧␈↓be␈αchosen␈αso␈αas␈αto␈αachieve␈αthe␈αminimum.␈α Still␈αothers␈αare␈αparameters.␈α They␈αare␈αnot␈αvaried␈αin␈αthe

␈↓ α∧␈↓minimization␈α⊂process,␈α⊂and␈α⊂therefore␈α⊂the␈α⊂minimum␈α∂obtained␈α⊂and␈α⊂the␈α⊂values␈α⊂of␈α⊂the␈α∂minimizing

␈↓ α∧␈↓variables␈α⊃depend␈α⊂on␈α⊃the␈α⊃values␈α⊂of␈α⊃the␈α⊂parameters.␈α⊃ We␈α⊃will␈α⊂point␈α⊃out␈α⊂the␈α⊃variables␈α⊃and␈α⊂the

␈↓ α∧␈↓parameters in the subsequent examples.

␈↓ α∧␈↓␈↓ αTIn␈α⊃some␈α⊃of␈α⊃the␈α⊃literature,␈α⊃it␈α⊂has␈α⊃been␈α⊃supposed␈α⊃that␈α⊃non-monotonic␈α⊃reasoning␈α⊂involves
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u4


␈↓ α∧␈↓giving␈α⊂all␈α∂predicates␈α⊂their␈α∂minimum␈α⊂extension.␈α∂ This␈α⊂mistake␈α∂has␈α⊂led␈α∂to␈α⊂theorems␈α⊂about␈α∂what

␈↓ α∧␈↓reasoning␈α
cannot␈αbe␈α
done␈αthat␈α
are␈α
irrelevant␈αto␈α
AI␈αand␈α
database␈αtheory,␈α
because␈α
their␈αpremisses

␈↓ α∧␈↓are too narrow.



␈↓ α∧␈↓3. ␈↓αA typology of uses of non-monotonic reasoning␈↓

␈↓ α∧␈↓␈↓ αTEach␈α∞of␈α∞the␈α∂several␈α∞papers␈α∞that␈α∂introduces␈α∞a␈α∞mode␈α∂of␈α∞non-monotonic␈α∞reasoning␈α∂seems␈α∞to

␈↓ α∧␈↓have␈αa␈αparticular␈αapplication␈αin␈αmind.␈α Perhaps␈αwe␈αare␈αlooking␈αat␈αdifferent␈αparts␈αof␈αan␈αelephant.

␈↓ α∧␈↓Therefore,␈α∞before␈α∞proceeding␈α∂to␈α∞applications␈α∞of␈α∂circumscription␈α∞I␈α∞want␈α∂to␈α∞suggest␈α∞a␈α∂typology␈α∞of

␈↓ α∧␈↓uses␈α
of␈α
non-monotonic␈α
reasoning.␈α
 The␈α
orientation␈αis␈α
towards␈α
circumscription,␈α
but␈α
I␈α
suppose␈αthe

␈↓ α∧␈↓considerations apply to other formalisms as well.

␈↓ α∧␈↓Non-monotonic reasoning has several uses.

␈↓ α∧␈↓1.␈αAs␈αa␈αcommunication␈αconvention.␈α Suppose␈αA␈αtells␈αB␈αabout␈αa␈αsituation␈αinvolving␈αa␈αbird.␈α If␈αthe

␈↓ α∧␈↓bird␈αcannot␈αfly,␈αand␈αthis␈αis␈αrelevant,␈αthen␈αA␈αmust␈αsay␈αso.␈α Whereas␈αif␈αthe␈αbird␈αcan␈αfly,␈αthere␈αis␈αno

␈↓ α∧␈↓requirement␈α
to␈α
mention␈α
the␈α
fact.␈α
 For␈αexample,␈α
if␈α
I␈α
hire␈α
you␈α
to␈αbuild␈α
me␈α
a␈α
bird␈α
cage␈α
and␈αyou␈α
don't

␈↓ α∧␈↓put␈αa␈αtop␈αon␈αit,␈αI␈αcan␈αget␈αout␈αof␈αpaying␈αfor␈αit␈αeven␈αif␈αyou␈αtell␈αthe␈αjudge␈αthat␈αI␈αnever␈αsaid␈αmy␈αbird

␈↓ α∧␈↓could␈α
fly.␈α However,␈α
if␈αI␈α
complain␈αthat␈α
you␈αwasted␈α
money␈αputting␈α
a␈αtop␈α
on␈αa␈α
cage␈αI␈α
intended␈αfor␈α
a

␈↓ α∧␈↓penguin, the judge will agree with you that if the bird couldn't fly I should have said so.

␈↓ α∧␈↓2.␈α⊂As␈α⊂a␈α⊃database␈α⊂or␈α⊂information␈α⊂storage␈α⊃convention.␈α⊂ It␈α⊂may␈α⊂be␈α⊃a␈α⊂convention␈α⊂of␈α⊃a␈α⊂particular

␈↓ α∧␈↓database␈αthat␈αcertain␈αpredicates␈αhave␈α
their␈αminimal␈αextension.␈α This␈αgeneralizes␈αthe␈α
closed␈αworld

␈↓ α∧␈↓assumption.␈α∀ When␈α∃a␈α∀database␈α∀makes␈α∃the␈α∀closed␈α∃world␈α∀assumption␈α∀for␈α∃all␈α∀predicates␈α∃it␈α∀is

␈↓ α∧␈↓reasonable␈α
to␈α
imbed␈αthis␈α
fact␈α
in␈α
the␈αprograms␈α
that␈α
use␈α
the␈αdatabase.␈α
 However,␈α
when␈α
only␈αsome

␈↓ α∧␈↓predicates␈α⊃are␈α∩to␈α⊃be␈α∩minimized,␈α⊃we␈α⊃need␈α∩to␈α⊃say␈α∩which␈α⊃ones␈α⊃by␈α∩appropriate␈α⊃sentences␈α∩of␈α⊃the

␈↓ α∧␈↓database,␈α
perhaps␈α
as␈α
a␈α
preamble␈α
to␈α
the␈αcollection␈α
of␈α
ground␈α
sentences␈α
that␈α
usually␈α
constitute␈αthe

␈↓ α∧␈↓main content.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u5


␈↓ α∧␈↓␈↓ αTNeither␈α1␈α
nor␈α2␈αrequires␈α
that␈αmost␈αbirds␈α
can␈αfly.␈α Should␈α
it␈αhappen␈αthat␈α
most␈αbirds␈αthat␈α
are

␈↓ α∧␈↓subject␈αto␈αthe␈αcommunication␈αor␈αabout␈αwhich␈αinformation␈αis␈αrequested␈αfrom␈αthe␈αdata␈αbase␈αcannot

␈↓ α∧␈↓fly, the convention may lead to inefficiency but not incorrectness.

␈↓ α∧␈↓3.␈αAs␈α
a␈αrule␈α
of␈αconjecture.␈α
 This␈αuse␈αwas␈α
emphasized␈αin␈α
(McCarthy␈α1980).␈α
 The␈αcircumscriptions

␈↓ α∧␈↓may␈αbe␈αregarded␈αas␈αexpressions␈αof␈αsome␈αprobabilistic␈αnotions␈αsuch␈αas␈α"most␈αbirds␈αcan␈αfly"␈αor␈αthey

␈↓ α∧␈↓may␈αbe␈α
expressions␈αof␈αstandard␈α
cases.␈α Thus␈α
it␈αis␈αsimple␈α
to␈αconjecture␈αthat␈α
there␈αare␈α
no␈αrelevant

␈↓ α∧␈↓present␈α⊂material␈α⊂objects␈α⊂other␈α⊂than␈α∂those␈α⊂whose␈α⊂presence␈α⊂can␈α⊂be␈α∂inferred.␈α⊂ It␈α⊂is␈α⊂also␈α⊂a␈α∂simple

␈↓ α∧␈↓conjecture␈α
that␈α∞a␈α
tool␈α∞asserted␈α
to␈α
be␈α∞present␈α
is␈α∞usable␈α
for␈α
its␈α∞normal␈α
function.␈α∞ Such␈α
conjectures

␈↓ α∧␈↓sometimes␈α∂conflict,␈α⊂but␈α∂there␈α∂is␈α⊂nothing␈α∂wrong␈α∂with␈α⊂having␈α∂incompatible␈α∂conjectures␈α⊂on␈α∂hand.

␈↓ α∧␈↓Besides␈α
the␈αpossibility␈α
of␈αdeciding␈α
that␈αone␈α
is␈αcorrect␈α
and␈α
the␈αother␈α
wrong,␈αit␈α
is␈αpossible␈α
to␈αuse␈α
one

␈↓ α∧␈↓for generating possible exceptions to the other.

␈↓ α∧␈↓4.␈α
As␈α
a␈αrepresentation␈α
of␈α
a␈αpolicy.␈α
 The␈α
example␈αis␈α
Doyle's␈α
"The␈αmeeting␈α
will␈α
be␈α
on␈αWednesday

␈↓ α∧␈↓unless another decision is explicitly made".  Again probabilities are not involved.

␈↓ α∧␈↓5.␈α∂As␈α∂a␈α⊂very␈α∂streamlined␈α∂expression␈α∂of␈α⊂probabilistic␈α∂information␈α∂when␈α⊂numerical␈α∂probabilities,

␈↓ α∧␈↓especially␈α⊗conditional␈α∃probabilities,␈α⊗are␈α∃unobtainable.␈α⊗ Since␈α∃circumscription␈α⊗doesn't␈α∃provide

␈↓ α∧␈↓numerical␈α∃probabilities,␈α∃its␈α∃probabilistic␈α∃interpretation␈α∃involves␈α∃probabilities␈α∃that␈α∃are␈α∀either

␈↓ α∧␈↓infinitesimal,␈αwithin␈αan␈αinfinitesimal␈αof␈αone,␈αor␈αintermediate␈α-␈αwithout␈αany␈αdiscrimination␈αamong

␈↓ α∧␈↓the␈αintermediate␈αvalues.␈α The␈αcircumscriptions␈αgive␈αconditional␈αprobabilities.␈α Thus␈αwe␈α
may␈αtreat

␈↓ α∧␈↓the␈α
probability␈αthat␈α
a␈αbird␈α
can't␈α
fly␈αas␈α
an␈αinfinitesimal.␈α
 However,␈α
if␈αthe␈α
rare␈αevent␈α
occurs␈αthat␈α
the

␈↓ α∧␈↓bird␈α
is␈αa␈α
penguin,␈α
then␈αthe␈α
conditional␈α
probability␈αthat␈α
it␈α
can␈αfly␈α
is␈α
infinitesimal,␈αbut␈α
we␈αmay␈α
hear

␈↓ α∧␈↓of some rare condition that would allow it to fly after all.

␈↓ α∧␈↓␈↓ αTWhy␈αdon't␈α
we␈αuse␈α
finite␈αprobabilities␈α
combined␈αby␈α
the␈αusual␈α
laws?␈α That␈α
would␈αbe␈α
fine␈αif

␈↓ α∧␈↓we␈α
had␈α
the␈α
numbers,␈α
but␈α
circumscription␈α
is␈α
usable␈αwhen␈α
we␈α
can't␈α
get␈α
the␈α
numbers␈α
or␈α
find␈αtheir

␈↓ α∧␈↓use␈αinconvenient.␈α Note␈α
that␈αthe␈αgeneral␈αprobability␈α
that␈αa␈αbird␈αcan␈α
fly␈αmay␈αbe␈αirrelevant,␈α
because
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u6


␈↓ α∧␈↓we␈α
are␈α
interested␈α
in␈α
the␈α
facts␈α
that␈α
influence␈αour␈α
opinion␈α
about␈α
whether␈α
a␈α
particular␈α
bird␈α
can␈αfly␈α
in

␈↓ α∧␈↓a particular situation.

␈↓ α∧␈↓␈↓ αTMoreover,␈α⊂the␈α⊂use␈α⊂of␈α⊂probabilities␈α⊂is␈α⊂normally␈α⊂considered␈α⊂to␈α⊂require␈α⊂the␈α⊂definition␈α⊂of␈α∂a

␈↓ α∧␈↓sample␈α
space,␈α
i.e.␈α
the␈αspace␈α
of␈α
all␈α
possibilities.␈α
 Circumscription␈αallows␈α
one␈α
to␈α
conjecture␈α
that␈αthe

␈↓ α∧␈↓cases␈α
we␈α
know␈α
about␈α
are␈α
all␈α
that␈α
there␈α
are.␈α
 However,␈α
when␈α
additional␈α
cases␈α
are␈α
found,␈αthe␈α
axioms

␈↓ α∧␈↓don't have to be changed.  Thus there is no fixed space of all possibilities.

␈↓ α∧␈↓␈↓ αTNotice␈α∞also␈α
that␈α∞circumscription␈α
does␈α∞not␈α∞provide␈α
for␈α∞weighing␈α
evidence;␈α∞it␈α∞is␈α
appropriate

␈↓ α∧␈↓when␈αthe␈αinformation␈αpermits␈αsnap␈αdecisions.␈α However,␈αmany␈αcases␈αnominally␈αtreated␈αin␈αterms␈αof

␈↓ α∧␈↓weighing␈α∞information␈α∞are␈α∂in␈α∞fact␈α∞cases␈α∂in␈α∞which␈α∞the␈α∞weights␈α∂are␈α∞such␈α∞that␈α∂circumscription␈α∞and

␈↓ α∧␈↓other defaults work better.

␈↓ α∧␈↓6.␈αAuto-epistemic␈αreasoning.␈α "If␈αI␈α
had␈αan␈αelder␈αbrother,␈αI'd␈α
know␈αit".␈α This␈αhas␈αbeen␈α
studied␈αby

␈↓ α∧␈↓R. Moore.  Perhaps it can be handled by circumscription.

␈↓ α∧␈↓7.␈αBoth␈αcommon␈α
sense␈αphysics␈αand␈α
common␈αsense␈αpsychology␈α
use␈αnon-monotonic␈αrules.␈α An␈α
object

␈↓ α∧␈↓will␈α
continue␈αin␈α
a␈αstraight␈α
line␈α
if␈αnothing␈α
interferes␈αwith␈α
it.␈α
 A␈αperson␈α
will␈αeat␈α
when␈αhungry␈α
unless

␈↓ α∧␈↓something␈α∪prevents␈α∩it.␈α∪ Such␈α∪rules␈α∩are␈α∪open␈α∩ended␈α∪about␈α∪what␈α∩might␈α∪prevent␈α∪the␈α∩expected

␈↓ α∧␈↓behavior,␈α
and␈α
this␈α∞is␈α
required,␈α
because␈α
we␈α∞are␈α
always␈α
encountering␈α
unexpected␈α∞phenomena␈α
that

␈↓ α∧␈↓modify␈α∂the␈α∂operation␈α∂of␈α∂our␈α∂rules.␈α∂ Science,␈α∂as␈α∂distinct␈α∂from␈α∂common␈α∂sense,␈α∂tries␈α∂to␈α∂work␈α∞with

␈↓ α∧␈↓exceptionless␈α⊂rules.␈α⊂ However,␈α⊂this␈α⊂means␈α⊂that␈α⊂common␈α⊂sense␈α⊂reasoning␈α⊂has␈α⊂to␈α⊂decide␈α⊃when␈α⊂a

␈↓ α∧␈↓scientific␈α
model␈α
is␈αapplicable,␈α
i.e.␈α
that␈α
there␈αare␈α
no␈α
important␈αphenomena␈α
not␈α
taken␈α
into␈αaccount

␈↓ α∧␈↓by the theories being used and the model of the particular phenomena.

␈↓ α∧␈↓␈↓ αTSeven␈α∩different␈α∩uses␈α∩for␈α∩non-monotonic␈α∪reasoning␈α∩seem␈α∩too␈α∩many,␈α∩so␈α∩perhaps␈α∪we␈α∩can

␈↓ α∧␈↓condense later.



␈↓ α∧␈↓4. ␈↓αMinimizing abnormality␈↓
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u7


␈↓ α∧␈↓␈↓ αTMany␈α⊂people␈α⊂have␈α⊂proposed␈α⊂representing␈α⊂facts␈α⊂about␈α⊂what␈α⊂is␈α⊂"normally"␈α⊂the␈α⊂case.␈α⊂ One

␈↓ α∧␈↓problem␈αis␈αthat␈αevery␈αobject␈αis␈αabnormal␈αin␈αsome␈αway,␈αand␈αwe␈αwant␈αto␈αallow␈αsome␈αaspects␈αof␈αthe

␈↓ α∧␈↓object␈αto␈αbe␈αabnormal␈αand␈αstill␈αassume␈αthe␈αnormality␈αof␈αthe␈αrest.␈α We␈αdo␈αthis␈αwith␈αa␈αpredicate␈α␈↓↓ab␈↓

␈↓ α∧␈↓standing␈α
for␈α
"abnormal".␈α We␈α
circumscribe␈α
␈↓↓ab z␈↓.␈α The␈α
argument␈α
of␈α␈↓↓ab␈↓␈α
will␈α
be␈αsome␈α
aspect␈α
of␈αthe

␈↓ α∧␈↓entities␈α
involved.␈α Some␈α
aspects␈α
can␈αbe␈α
abnormal␈α
without␈αaffecting␈α
others.␈α
 The␈αaspects␈α
themselves

␈↓ α∧␈↓are abstract entities, and their unintuitiveness is somewhat a blemish on the theory.

␈↓ α∧␈↓␈↓ αTThere are many applications.



␈↓ α∧␈↓5. ␈↓αWhether birds can fly␈↓

␈↓ α∧␈↓␈↓ αTMarvin␈α~Minsky␈α~(1982)␈α~offered␈α~expressing␈α~the␈α~facts␈α~and␈α~non-monotonic␈α→reasoning

␈↓ α∧␈↓concerning␈α⊂the␈α⊂ability␈α⊂of␈α⊂birds␈α⊂to␈α⊂fly␈α⊂as␈α∂a␈α⊂challenge␈α⊂to␈α⊂advocates␈α⊂of␈α⊂formal␈α⊂systems␈α⊂based␈α∂on

␈↓ α∧␈↓mathematical logic.

␈↓ α∧␈↓␈↓ αTThere␈α
are␈α
many␈α
ways␈α
of␈α
non-monotonically␈α
axiomatizing␈α
the␈α
facts␈α
about␈α
which␈α∞birds␈α
can

␈↓ α∧␈↓fly.  The following set of axioms using ␈↓↓ab␈↓ seems to me quite straightforward.

␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Unless␈αan␈αobject␈αis␈αabnormal␈αin␈α␈↓↓aspect1,␈↓␈αit␈αcan't␈αfly.␈α (We're␈αusing␈αa␈αconvention␈αthat␈αparentheses

␈↓ α∧␈↓may␈α∪be␈α∀omitted␈α∪for␈α∪functions␈α∀and␈α∪predicates␈α∀of␈α∪one␈α∪argument,␈α∀so␈α∪that␈α∪(2)␈α∀is␈α∪the␈α∀same␈α∪as

␈↓ α∧␈↓␈↓↓∀x.(¬ab(aspect1(x) ⊃ ¬flies(x))␈↓.)

␈↓ α∧␈↓␈↓ αTNote␈α
that␈α
it␈α
wouldn't␈α
work␈α
to␈α
write␈α
␈↓↓ab␈α
x␈↓␈α
instead␈α
of␈α
␈↓↓ab␈α
aspect1␈α
x␈↓,␈α
because␈α
we␈α
don't␈α∞want␈α
a

␈↓ α∧␈↓bird␈α⊂that␈α⊂is␈α⊂abnormal␈α⊂with␈α⊂respect␈α⊂to␈α⊂its␈α⊂ability␈α⊂to␈α⊂fly␈α⊂to␈α⊂be␈α⊂automatically␈α⊂abnormal␈α⊂in␈α⊂other

␈↓ α∧␈↓respects.  Using aspects limits the effects of proofs of abnormality.

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓A␈αbird␈αis␈αabnormal␈αin␈α
␈↓↓aspect1,␈↓␈αso␈α(2)␈αcan't␈αbe␈α
used␈αto␈αshow␈αit␈αcan't␈α
fly.␈α If␈α(3)␈αwere␈αomitted,␈α
when

␈↓ α∧␈↓we␈α∩did␈α∩the␈α∩circumscription␈α∩we␈α⊃would␈α∩only␈α∩be␈α∩able␈α∩to␈α⊃infer␈α∩a␈α∩disjunction.␈α∩ Either␈α∩a␈α∩bird␈α⊃is
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u8


␈↓ α∧␈↓abnormal␈α∞in␈α
␈↓↓aspect1␈↓␈α∞or␈α
it␈α∞can␈α
fly␈α∞unless␈α
it␈α∞is␈α
abnormal␈α∞in␈α
␈↓↓aspect2.␈↓␈α∞(3)␈α
establishes␈α∞expresses␈α
our

␈↓ α∧␈↓preference␈α∂for␈α∞inferring␈α∂that␈α∞a␈α∂bird␈α∞is␈α∂abnormal␈α∞in␈α∂␈↓↓aspect1␈↓␈α∞rather␈α∂than␈α∞␈↓↓aspect2.␈↓␈α∂We␈α∞call␈α∂(3)␈α∞a

␈↓ α∧␈↓␈↓↓cancellation of inheritance␈↓ axiom.  We will see more of them.

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓Unless a bird is abnormal in ␈↓↓aspect2,␈↓ it can fly.

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Ostriches␈α
are␈α
abnormal␈α
in␈α
␈↓↓aspect2.␈↓␈α
This␈α
doesn't␈α
say␈αthat␈α
an␈α
ostrich␈α
cannot␈α
fly␈α
-␈α
merely␈α
that␈α(4)

␈↓ α∧␈↓can't be used to infer that it does.  (5) is another cancellation of inheritance axiom.

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x.penguin x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓Penguins are also abnormal in ␈↓↓aspect2.␈↓

␈↓ α∧␈↓7)␈↓ αt ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x.penguin x ∧¬ab aspect4 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Normally␈α∞ostriches␈α∂and␈α∞penguins␈α∞can't␈α∂fly.␈α∞ However,␈α∞there␈α∂is␈α∞an␈α∞out.␈α∂ (7)␈α∞and␈α∞(8)␈α∂provide␈α∞that

␈↓ α∧␈↓under␈α⊃unspecified␈α⊃conditions,␈α⊃an␈α⊃ostrich␈α⊃or␈α⊃penguin␈α⊃might␈α⊃fly␈α⊃after␈α⊃all.␈α⊃ If␈α⊃we␈α⊃give␈α∩no␈α⊃such

␈↓ α∧␈↓conditions,␈αwe␈α
will␈αconclude␈α
that␈αan␈α
ostrich␈αor␈α
penguin␈αcan't␈α
fly.␈α Additional␈α
objects␈αthat␈α
can␈αfly

␈↓ α∧␈↓may␈α∂be␈α∂specified.␈α⊂ Each␈α∂needs␈α∂two␈α∂axioms.␈α⊂ The␈α∂first␈α∂says␈α∂that␈α⊂it␈α∂is␈α∂abnormal␈α∂in␈α⊂␈↓↓aspect1␈↓␈α∂and

␈↓ α∧␈↓prevents␈α(2)␈αfrom␈αbeing␈αused␈αto␈αsay␈αthat␈αit␈αcan't␈αfly.␈α The␈αsecond␈αprovides␈αthat␈αit␈αcan␈αfly␈αunless␈αit

␈↓ α∧␈↓is␈α
abnormal␈αin␈α
yet␈αanother␈α
way.␈α
 Additional␈αnon-flying␈α
birds␈αcan␈α
also␈α
be␈αprovided␈α
for␈αat␈α
a␈αcost␈α
of

␈↓ α∧␈↓two axioms per kind.

␈↓ α∧␈↓␈↓ αTWe␈α
haven't␈αyet␈α
said␈αthat␈α
ostriches␈αand␈α
penguins␈αare␈α
birds,␈αso␈α
let's␈αdo␈α
that␈αand␈α
throw␈αin␈α
that

␈↓ α∧␈↓canaries are birds also.

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀x.ostrich x ⊃ bird x␈↓

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀x.penguin x ⊃ bird x␈↓

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀x.canary x ∧ ¬ab aspect5 x ⊃ bird x␈↓.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ u9


␈↓ α∧␈↓We␈α∂threw␈α∂in␈α⊂␈↓↓aspect5␈↓␈α∂just␈α∂in␈α⊂case␈α∂one␈α∂wanted␈α⊂to␈α∂use␈α∂the␈α⊂term␈α∂canary␈α∂in␈α⊂the␈α∂sense␈α∂of␈α⊂a␈α∂1930s

␈↓ α∧␈↓gangster movie.

␈↓ α∧␈↓Asserting␈α
that␈α
ostriches,␈α
penguins␈α
and␈α
canaries␈α∞are␈α
birds␈α
will␈α
help␈α
inherit␈α
other␈α∞properties␈α
from

␈↓ α∧␈↓the class of birds.  For example, we have

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀x. bird x ∧ ¬ab aspect6 x ⊃ feathered x␈↓.

␈↓ α∧␈↓So␈αfar␈αthere␈α
is␈αnothing␈αto␈α
prevent␈αostriches,␈αpenguins␈αand␈α
canaries␈αfrom␈αoverlapping.␈α
 We␈αcould

␈↓ α∧␈↓write disjointness axioms like

␈↓ α∧␈↓13)␈↓ αt␈↓↓∀x. ¬ostrich x ∨ ¬penguin x␈↓,

␈↓ α∧␈↓but␈α
we␈α
would␈α
require␈α
␈↓↓n␈↓∧2␈↓␈α
of␈α
them␈α
if␈α
we␈α
have␈α
␈↓↓n␈↓␈α
species.␈α
 This␈α
problem␈α
is␈α
like␈α
the␈α
unique␈αnames

␈↓ α∧␈↓problem.

␈↓ α∧␈↓␈↓ αTIf␈αthese␈αare␈αthe␈αonly␈αfacts␈αto␈αbe␈αtaken␈αinto␈αaccount,␈αwe␈αmust␈αsomehow␈αspecify␈αthat␈αwhat␈αcan

␈↓ α∧␈↓fly␈α⊂is␈α⊂to␈α⊂be␈α⊂determined␈α⊂by␈α⊂circumscribing␈α⊂the␈α⊂wff␈α⊂␈↓↓ab z␈↓␈α⊂using␈α⊂␈↓↓ab␈↓␈α⊂and␈α⊂␈↓↓flies␈↓␈α⊂as␈α⊂variables.␈α⊂ Why

␈↓ α∧␈↓exactly␈α
these?␈α∞ If␈α
␈↓↓ab␈↓␈α∞were␈α
not␈α∞taken␈α
as␈α∞variable,␈α
␈↓↓ab z␈↓␈α∞couldn't␈α
vary␈α∞either,␈α
and␈α∞the␈α
minimization

␈↓ α∧␈↓problem␈α
would␈α
go␈α
away.␈α
 Since␈α
the␈α
purpose␈α
of␈α
the␈α
axiom␈α
set␈α
is␈α
to␈α
describe␈α
what␈α
flies,␈α
the␈α
predicate

␈↓ α∧␈↓␈↓↓flies␈↓␈αmust␈αbe␈αvaried␈αalso.␈α Suppose␈αwe␈αcontemplate␈αtaking␈α␈↓↓bird␈↓␈αas␈αvariable␈αalso.␈α In␈αthe␈αfirst␈αplace,

␈↓ α∧␈↓this␈αviolates␈αan␈αintuition␈αthat␈αdeciding␈αwhat␈α
flies␈αfollows␈αdeciding␈αwhat␈αis␈αa␈αbird␈αin␈α
the␈αcommon

␈↓ α∧␈↓sense␈α
situations␈α
we␈α
want␈αto␈α
cover.␈α
 Secondly,␈α
if␈αwe␈α
use␈α
exactly␈α
the␈αabove␈α
axioms␈α
and␈α
admit␈αbird␈α
as

␈↓ α∧␈↓a␈α⊂variable,␈α⊂we␈α⊃will␈α⊂further␈α⊂conclude␈α⊃that␈α⊂the␈α⊂only␈α⊂birds␈α⊃are␈α⊂penguins,␈α⊂canaries␈α⊃and␈α⊂ostriches.

␈↓ α∧␈↓Namely,␈α⊃for␈α⊃these␈α⊃entities␈α⊃something␈α⊃has␈α⊂to␈α⊃be␈α⊃abnormal,␈α⊃and␈α⊃therefore␈α⊃minimizing␈α⊃␈↓↓ab z␈↓␈α⊂will

␈↓ α∧␈↓involve␈α⊂making␈α⊂as␈α∂few␈α⊂entities␈α⊂as␈α⊂possible␈α∂penguins,␈α⊂canaries␈α⊂and␈α∂ostriches.␈α⊂ If␈α⊂we␈α⊂also␈α∂admit

␈↓ α∧␈↓␈↓↓penguin,␈↓␈α␈↓↓ostrich,␈↓␈αand␈α␈↓↓canary␈↓␈αas␈αvariable,␈αwe␈αwill␈αsucceed␈αin␈αmaking␈α␈↓↓ab z␈↓␈αalways␈αfalse,␈αand␈αthere

␈↓ α∧␈↓will be no birds at all.

␈↓ α∧␈↓␈↓ αTHowever,␈α
if␈αthe␈α
same␈α
circumscriptions␈αare␈α
done␈α
with␈αadditional␈α
axioms␈α
like␈α␈↓↓canary Tweety␈↓

␈↓ α∧␈↓and␈α␈↓↓ostrich Joe,␈↓␈α
we␈αwill␈α
get␈αthe␈α
expected␈αresult␈αthat␈α
Tweety␈αcan␈α
fly␈αand␈α
Joe␈αcannot␈α
even␈αif␈αall␈α
the

␈↓ α∧␈↓above are variable.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f10


␈↓ α∧␈↓␈↓ αTWhile␈α∩this␈α∩works␈α∩it␈α∩may␈α∩be␈α∩more␈α⊃straightforward,␈α∩and␈α∩therefore␈α∩less␈α∩likely␈α∩to␈α∩lead␈α⊃to

␈↓ α∧␈↓subsequent trouble, to circumscribe birds, ostriches and penguins with axioms like

␈↓ α∧␈↓14)␈↓ αt ␈↓↓∀x.¬ab aspect8 x ⊃ ¬bird x␈↓, etc.

␈↓ α∧␈↓␈↓ αTWe␈αhave␈αnot␈αyet␈αspecified␈αhow␈αa␈αprogram␈αwill␈αknow␈αwhat␈αto␈αcircumscribe.␈α One␈αextreme␈αis

␈↓ α∧␈↓to␈α
build␈αit␈α
into␈αthe␈α
program,␈αbut␈α
this␈αis␈α
contrary␈αto␈α
the␈αdeclarative␈α
spirit.␈α However,␈α
a␈αstatement␈α
of

␈↓ α∧␈↓what␈αto␈αcircumscribe␈αisn't␈αjust␈αa␈αsentence␈αof␈αthe␈αlanguage␈αbecause␈αof␈αits␈αnon-monotonic␈αcharacter.

␈↓ α∧␈↓My␈αpresent,␈αadmittedly␈αsomewhat␈αunsatisfactory,␈αidea␈αis␈αto␈αinclude␈αsome␈αsort␈αof␈αmetamathematical

␈↓ α∧␈↓statement like

␈↓ α∧␈↓15)␈↓ αt ␈↓↓circumsribe(ab z; ab, flies, bird, ostrich, penguin)␈↓

␈↓ α∧␈↓in␈α⊂a␈α⊂"policy"␈α⊂database␈α⊂available␈α⊃to␈α⊂the␈α⊂program.␈α⊂ (15)␈α⊂is␈α⊂intended␈α⊃to␈α⊂mean␈α⊂that␈α⊂␈↓↓ab z␈↓␈α⊂is␈α⊃to␈α⊂be

␈↓ α∧␈↓circumscribed␈α
with␈α
␈↓↓ab,␈↓␈α
␈↓↓flies,␈↓␈α
␈↓↓bird,␈↓␈α
␈↓↓ostrich␈↓␈α
and␈α
␈↓↓penguin␈↓␈α
taken␈α
as␈α
variable.␈α
 Explicitly␈α
listing␈α
the

␈↓ α∧␈↓variables␈α∪makes␈α∀adding␈α∪new␈α∪kinds␈α∀awkward,␈α∪since␈α∪they␈α∀will␈α∪have␈α∪to␈α∀be␈α∪mentioned␈α∀in␈α∪the

␈↓ α∧␈↓␈↓↓circumscribe␈↓ statement.


␈↓ α∧␈↓6. ␈↓αThe unique names hypothesis␈↓

␈↓ α∧␈↓␈↓ αTRaymond␈α↔Reiter␈α_(1980b)␈α↔introduced␈α_the␈α↔phrase␈α↔"unique␈α_names␈α↔hypothesis"␈α_for␈α↔the

␈↓ α∧␈↓assumption␈α
each␈α
object␈α
has␈α
a␈α
unique␈α
name,␈α
i.e.␈α
 that␈α
distinct␈α
names␈α
denote␈α
distinct␈α∞objects.␈α
 We

␈↓ α∧␈↓want␈αto␈αtreat␈αthis␈αnon-monotonically.␈α Namely,␈αwe␈αwant␈αa␈αwff␈αthat␈αpicks␈αout␈αthose␈αmodels␈α
of␈αour

␈↓ α∧␈↓initial␈α
assumptions␈α
maximize␈αthe␈α
inequality␈α
of␈αthe␈α
denotations␈α
of␈αconstant␈α
symbols.␈α
 While␈αwe're

␈↓ α∧␈↓at␈α∂it,␈α∞we␈α∂might␈α∂as␈α∞well␈α∂try␈α∂for␈α∞something␈α∂stronger.␈α∂ We␈α∞want␈α∂to␈α∂maximize␈α∞the␈α∂extent␈α∂to␈α∞which

␈↓ α∧␈↓distinct␈α∩terms␈α∩designate␈α⊃distinct␈α∩objects.␈α∩ When␈α∩there␈α⊃is␈α∩a␈α∩unique␈α⊃model␈α∩of␈α∩the␈α∩axioms␈α⊃that

␈↓ α∧␈↓maximizes␈α∂distinctness,␈α∂we␈α∞can␈α∂put␈α∂it␈α∂more␈α∞simply;␈α∂two␈α∂terms␈α∞denote␈α∂distinct␈α∂objects␈α∂unless␈α∞the

␈↓ α∧␈↓axioms␈αforce␈αthem␈αto␈αdenote␈αthe␈αsame.␈α If␈αwe␈αare␈αeven␈αmore␈αfortunate,␈αas␈αwe␈αare␈αin␈αthe␈αexamples

␈↓ α∧␈↓to be given, we can say that two terms denote distinct objects unless their equality is provable.

␈↓ α∧␈↓␈↓ αTWe␈α∩don't␈α∩know␈α∩a␈α∩completely␈α∩satisfactory␈α∩way␈α⊃of␈α∩doing␈α∩this.␈α∩ Suppose␈α∩that␈α∩we␈α∩have␈α⊃a
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f11


␈↓ α∧␈↓language␈α∂␈↓↓L␈↓␈α∂and␈α∂a␈α∂theory␈α∂␈↓↓T␈↓␈α∂consisting␈α∂of␈α⊂the␈α∂consequences␈α∂of␈α∂a␈α∂formula␈α∂␈↓↓A.␈↓␈α∂It␈α∂would␈α⊂be␈α∂most

␈↓ α∧␈↓pleasant␈α
if␈α∞we␈α
could␈α
just␈α∞circumscribe␈α
equality,␈α
but␈α∞as␈α
Reiter␈α
and␈α∞Etherington␈α
(to␈α∞be␈α
published)

␈↓ α∧␈↓point␈α∂out,␈α∂this␈α∂doesn't␈α∂work,␈α∂and␈α∂nothing␈α∂similar␈α∂works.␈α∂ We␈α∂could␈α∂hope␈α∂to␈α∂circumscribe␈α∂some

␈↓ α∧␈↓other␈α∞formula␈α∞of␈α∞the␈α∞␈↓↓L,␈↓␈α∞but␈α∞this␈α∞doesn't␈α∞seem␈α∞to␈α∞work␈α∞either.␈α∞ Failing␈α∞that,␈α∞we␈α∞could␈α∂hope␈α∞for

␈↓ α∧␈↓some␈αother␈αsecond␈αorder␈αformula␈αtaken␈αfrom␈α␈↓↓L␈↓␈αthat␈αwould␈αexpress␈αthe␈αunique␈αnames␈αhypothesis,

␈↓ α∧␈↓but we don't presently see how to do it.

␈↓ α∧␈↓␈↓ αTOur␈α
solution␈α
involves␈αextending␈α
the␈α
language␈αby␈α
introducing␈α
the␈αnames␈α
themselves␈α
as␈αthe

␈↓ α∧␈↓only objects.  All assertions about objects are expressed as assertions about the names.

␈↓ α∧␈↓␈↓ αTWe␈αsuppose␈αour␈αtheory␈αis␈αsuch␈α
that␈αthe␈αnames␈αthemselves␈αare␈αall␈αprovably␈α
distinct.␈α There

␈↓ α∧␈↓are␈α
several␈α
ways␈α
of␈α
doing␈α
this.␈α
 Let␈α
the␈α
names␈αbe␈α
␈↓↓n1,␈↓␈α
␈↓↓n2,␈↓␈α
etc.␈α
 The␈α
simplest␈α
solution␈α
is␈α
to␈αhave␈α
an

␈↓ α∧␈↓axiom␈α␈↓↓ni ≠nj␈↓␈αfor␈αeach␈αpair␈αof␈αdistinct␈αnames.␈α This␈αrequires␈αa␈αnumber␈αof␈αaxioms␈αproportional␈αto

␈↓ α∧␈↓the␈α
square␈αof␈α
the␈α
number␈αof␈α
names,␈α
which␈αis␈α
sometimes␈α
objectionable.␈α The␈α
next␈αsolution␈α
involves

␈↓ α∧␈↓introducing␈α⊂an␈α⊂arbitrary␈α⊂ordering␈α∂on␈α⊂the␈α⊂names.␈α⊂ We␈α∂have␈α⊂special␈α⊂axioms␈α⊂␈↓↓n1 < n2,␈α∂n2 < n3,

␈↓ α∧␈↓↓n3 < n4␈↓,␈α∂etc.␈α∞and␈α∂the␈α∞general␈α∂axioms␈α∞␈↓↓∀x y.x < y ⊃ x ≠ y␈↓␈α∂and␈α∂␈↓↓∀x y z. x < y ∧ y < z ⊃ x < z␈↓.␈α∞ This

␈↓ α∧␈↓makes␈αthe␈αnumber␈α
of␈αaxioms␈αproportional␈α
to␈αthe␈αnumber␈αof␈α
names.␈α A␈αthird␈α
possibility␈αinvolves

␈↓ α∧␈↓mapping␈α∞the␈α
names␈α∞onto␈α∞integers␈α
with␈α∞axioms␈α
like␈α∞␈↓↓index n1 = 1,␈α∞index n2 = 2␈↓,␈α
etc.␈α∞and␈α∞using␈α
a

␈↓ α∧␈↓theory␈α
of␈α
the␈α
integers␈α
that␈α
provides␈α∞for␈α
their␈α
distinctness.␈α
 The␈α
fourth␈α
possibility␈α∞involves␈α
using

␈↓ α∧␈↓string␈α⊃constants␈α⊂for␈α⊃the␈α⊃names␈α⊂and␈α⊃"attaching"␈α⊃to␈α⊂equality␈α⊃in␈α⊃the␈α⊂language␈α⊃a␈α⊃subroutine␈α⊂that

␈↓ α∧␈↓computes␈α⊂whether␈α⊂two␈α⊂strings␈α⊂are␈α∂equal.␈α⊂ If␈α⊂our␈α⊂names␈α⊂were␈α∂quoted␈α⊂symbols␈α⊂as␈α⊂in␈α⊂LISP,␈α∂this

␈↓ α∧␈↓amounts␈α∂to␈α∂having␈α∂␈↓↓'a ≠ 'b␈↓␈α∂and␈α∂all␈α∂its␈α∞countable␈α∂infinity␈α∂of␈α∂analogs␈α∂as␈α∂axioms.␈α∂ Each␈α∂of␈α∞these

␈↓ α∧␈↓devices is useful in appropriate circumstances.

␈↓ α∧␈↓␈↓ αTFrom␈α∞the␈α∞point␈α∞of␈α
view␈α∞of␈α∞mathematical␈α∞logic,␈α
there␈α∞is␈α∞no␈α∞harm␈α
in␈α∞having␈α∞an␈α∞infinity␈α
of

␈↓ α∧␈↓such␈α∞axioms.␈α∞ From␈α∞the␈α∂computational␈α∞point␈α∞of␈α∞view␈α∞of␈α∂a␈α∞theorem␈α∞proving␈α∞or␈α∂problem␈α∞solving

␈↓ α∧␈↓program,␈α
we␈α
merely␈α
suppose␈α
that␈αwe␈α
rely␈α
on␈α
the␈α
computer␈αto␈α
generate␈α
the␈α
assertion␈α
that␈αtwo␈α
names
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f12


␈↓ α∧␈↓are␈α
distinct␈α
whenever␈α
this␈α
is␈α
required,␈α
since␈α
a␈α
subroutine␈α
can␈α
easily␈α
tell␈α
whether␈α
two␈α
strings␈αare␈α
the

␈↓ α∧␈↓same.

␈↓ α∧␈↓␈↓ αTBesides␈α∩axiomatizing␈α∩the␈α∩distinctness␈α∩of␈α∩the␈α∩constants,␈α∩we␈α∩also␈α∩want␈α∩to␈α∩axiomatize␈α∩the

␈↓ α∧␈↓distinctness␈α⊂of␈α⊂terms.␈α⊂ This␈α∂may␈α⊂be␈α⊂accomplished␈α⊂by␈α∂providing␈α⊂for␈α⊂each␈α⊂function␈α⊂two␈α∂axioms.

␈↓ α∧␈↓Letting ␈↓↓foo␈↓ be a function of two arguments we postulate

␈↓ α∧␈↓16)␈↓ αt ␈↓↓∀x1 x2 y1 y2.foo(x1,y1) = foo(x2,y2) ⊃ x1 = x2 ∧ y1 =y2␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓17)␈↓ αt ␈↓↓∀x y.fname foo(x,y) = 'foo␈↓.

␈↓ α∧␈↓The␈αfirst␈α
axiom␈αensures␈α
that␈αunless␈α
the␈αarguments␈αof␈α
␈↓↓foo␈↓␈αare␈α
identical,␈αits␈α
values␈αare␈αdistinct.␈α
 The

␈↓ α∧␈↓second␈α∞ensures␈α
that␈α∞the␈α∞values␈α
of␈α∞␈↓↓foo␈↓␈α∞are␈α
distinct␈α∞from␈α∞the␈α
values␈α∞of␈α∞any␈α
other␈α∞function␈α∞or␈α
any

␈↓ α∧␈↓constant, assuming that we refrain from naming any constant ␈↓↓'foo.␈↓

␈↓ α∧␈↓␈↓ αTThese␈α
axioms␈αamount␈α
to␈α
making␈αour␈α
domain␈αisomorphic␈α
to␈α
the␈αHerbrand␈α
universe␈α
of␈αthe

␈↓ α∧␈↓language.

␈↓ α∧␈↓␈↓ αTNow␈α⊃that␈α⊃the␈α⊃names␈α⊃are␈α⊃guaranteed␈α⊃distinct,␈α⊃what␈α⊃about␈α⊃the␈α⊃objects␈α⊃they␈α⊃denote?␈α⊂ We

␈↓ α∧␈↓introduce␈α∪a␈α∀predicate␈α∪␈↓↓e(x,y)␈↓␈α∪and␈α∀axiomatize␈α∪it␈α∀to␈α∪be␈α∪an␈α∀equivalence␈α∪relation.␈α∀ Its␈α∪intended

␈↓ α∧␈↓interpretation␈αis␈αthat␈αthe␈αnames␈α␈↓↓x␈↓␈αand␈α␈↓↓y␈↓␈αdenote␈αthe␈αsame␈αobject.␈α We␈αthen␈αformulate␈αall␈αour␈αusual

␈↓ α∧␈↓axioms␈αin␈αterms␈αof␈αnames␈αrather␈αthan␈αin␈αterms␈αof␈αobjects.␈α Thus␈α␈↓↓on(n1,n2)␈↓␈αmeans␈αthat␈αthe␈αobject

␈↓ α∧␈↓named␈α
by␈α
␈↓↓n1␈↓␈α
is␈α
on␈α
the␈α
object␈α
named␈α
by␈α
␈↓↓n2,␈↓␈α
and␈α
␈↓↓bird x␈↓␈α
means␈α
that␈α
the␈α
name␈α
␈↓↓x␈↓␈α
denotes␈α
a␈α
bird.

␈↓ α∧␈↓We␈α⊂add␈α⊂axioms␈α∂of␈α⊂substitutivity␈α⊂for␈α⊂␈↓↓e␈↓␈α∂with␈α⊂regard␈α⊂to␈α⊂those␈α∂predicates␈α⊂and␈α⊂functions␈α⊂that␈α∂are

␈↓ α∧␈↓translates␈αof␈αpredicates␈αreferring␈α
to␈αobjects␈αrather␈αthan␈α
predicates␈αon␈αthe␈αnames␈αthemselves.␈α
 Thus

␈↓ α∧␈↓we may have axioms

␈↓ α∧␈↓18)␈↓ αt ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (on(n1,n2) ≡ on(n1',n2')␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓19)␈↓ αt␈↓↓∀x1 x2 y1 y2.e(x1,x2) ∧ e(y1,y2) ⊃ e(foo(x1,y1),foo(x2,y2))␈↓.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f13


␈↓ α∧␈↓␈↓ αTIf␈αfor␈αsome␈αclass␈α␈↓↓C␈↓␈αof␈αnames,␈αwe␈αwish␈αto␈αassert␈αthe␈αunique␈αnames␈αhypothesis,␈αwe␈αsimply␈αuse

␈↓ α∧␈↓an axiom like

␈↓ α∧␈↓20)␈↓ αt ␈↓↓∀n1 n2.n1 ε C ∧ n2 ε C ⊃ (e(n1,n2) ≡ n1 = n2)␈↓.

␈↓ α∧␈↓␈↓ αTHowever,␈α
we␈α
often␈α
want␈αonly␈α
to␈α
assume␈α
that␈α
distinct␈αnames␈α
denote␈α
distinct␈α
objects␈αwhen␈α
this

␈↓ α∧␈↓doesn't␈αcontradict␈α
our␈αother␈αassumptions.␈α
 In␈αgeneral,␈α
our␈αaxioms␈αwon't␈α
permit␈αmaking␈α
all␈αnames

␈↓ α∧␈↓distinct␈α∂simultaneously,␈α⊂and␈α∂there␈α∂will␈α⊂be␈α∂several␈α∂models␈α⊂with␈α∂maximally␈α∂distinct␈α⊂objects.␈α∂ The

␈↓ α∧␈↓simplest example is obtained by circumscribing ␈↓↓e(x,y)␈↓ while adhering to the axiom

␈↓ α∧␈↓21)␈↓ αt ␈↓↓e(n1,n2) ∨ e(n1,n3)␈↓

␈↓ α∧␈↓where␈α∪␈↓↓n1,␈↓␈α∩␈↓↓n2,␈↓␈α∪and␈α∩␈↓↓n3␈↓␈α∪are␈α∩distinct␈α∪names.␈α∩ There␈α∪will␈α∩then␈α∪be␈α∩two␈α∪models,␈α∪one␈α∩satisfying

␈↓ α∧␈↓␈↓↓e(n1,n2) ∧ ¬e(n1,n3)␈↓ and the other satisfying ␈↓↓¬e(n1,n2) ∧ e(n1,n3).␈↓

␈↓ α∧␈↓␈↓ αTThus␈αcircumscribing␈α
␈↓↓e(x,y)␈↓␈αmaximizes␈α
uniqueness␈αof␈αnames.␈α
 If␈αwe␈α
only␈αwant␈αunique␈α
names

␈↓ α∧␈↓for␈αsome␈αclass␈α␈↓↓C␈↓␈αof␈αnames,␈αthen␈αwe␈αcircumscribe␈αthe␈αformula␈α␈↓↓x ε C ∧ y ε C ⊃ e(x,y)␈↓.␈α
 An␈αexample

␈↓ α∧␈↓of␈αsuch␈αa␈α
circumscription␈αis␈αgiven␈α
in␈αAppendix␈αB.␈α However,␈α
there␈αseems␈αto␈α
be␈αa␈αprice.␈α
 Part␈αof

␈↓ α∧␈↓the␈α
price␈αis␈α
admitting␈αnames␈α
as␈αobjects.␈α
 Another␈αpart␈α
is␈αadmitting␈α
the␈αpredicate␈α
␈↓↓e(x,y)␈↓␈α
which␈αis

␈↓ α∧␈↓substitutive␈αfor␈α
predicates␈αand␈αfunctions␈α
of␈αnames␈α
that␈αreally␈αare␈α
about␈αthe␈α
objects␈αdenoted␈αby␈α
the

␈↓ α∧␈↓names.␈α∂ ␈↓↓e(x,y)␈↓␈α∂is␈α∂not␈α∞to␈α∂be␈α∂taken␈α∂as␈α∞substitutive␈α∂for␈α∂predicates␈α∂on␈α∞names␈α∂that␈α∂aren't␈α∂about␈α∞the

␈↓ α∧␈↓objects.  Of these our only present example is equality.  Thus we don't have

␈↓ α∧␈↓* ␈↓↓∀n1 n2 n1' n2'.e(n1,n1') ∧ e(n2,n2') ⊃ (n1 = n2) ≡ n1' = n2')␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α
awkward␈αpart␈α
of␈αthe␈α
price␈αis␈α
that␈α
we␈αmust␈α
refrain␈αfrom␈α
any␈αfunctions␈α
whose␈αvalues␈α
are

␈↓ α∧␈↓the␈αobjects␈αthemselves␈αrather␈αthan␈αnames.␈α
 They␈αwould␈αspoil␈αthe␈αcircumscription␈αby␈α
not␈αallowing

␈↓ α∧␈↓us␈αto␈αinfer␈αthe␈αdistinctness␈αof␈αthe␈αobjects␈αdenoted␈αby␈αdistinct␈αnames.␈α Actually,␈αwe␈αcan␈αallow␈αthem

␈↓ α∧␈↓provided␈αwe␈αdon't␈αinclude␈αthe␈αaxioms␈αinvolving␈αthem␈αin␈αthe␈αcircumscription.␈α Unfortunately,␈αthis

␈↓ α∧␈↓spoils the other property of circumscription that lets us take any facts into account.

␈↓ α∧␈↓␈↓ αTThe␈α
examples␈α
of␈α
the␈α
use␈α
of␈α
circumscription␈α
in␈α
AI␈α
in␈α
the␈α
rest␈α
of␈α
the␈α
paper␈α
don't␈αinterpret␈α
the
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f14


␈↓ α∧␈↓variables␈α∞as␈α∞merely␈α∂ranging␈α∞over␈α∞names.␈α∞ Therefore,␈α∂they␈α∞are␈α∞incompatible␈α∞with␈α∂getting␈α∞unique

␈↓ α∧␈↓names␈αby␈αcircumscription␈αas␈αdescribed␈αin␈αthis␈αsection.␈α Presumably␈αit␈αwouldn't␈αbe␈αvery␈αdifficult␈αto

␈↓ α∧␈↓revise those axioms for compatibility with the present approach to unique names.


␈↓ α∧␈↓7. ␈↓αTwo examples of Raymond Reiter␈↓

␈↓ α∧␈↓␈↓ αTReiter␈α∃asks␈α∃about␈α∃representing,␈α∃"Quakers␈α∀are␈α∃normally␈α∃pacifists␈α∃and␈α∃Republicans␈α∀are

␈↓ α∧␈↓normally␈αnon-pacifists.␈α How␈αabout␈αNixon,␈αwho␈αis␈αboth␈αa␈αQuaker␈αand␈αa␈αRepublican?"␈αSystems␈αof

␈↓ α∧␈↓non-monotonic␈αreasoning␈α
that␈αuse␈α
non-provability␈αas␈α
a␈αbasis␈α
for␈αinferring␈α
negation␈αwill␈αinfer␈α
that

␈↓ α∧␈↓Nixon␈α∂is␈α∂neither␈α∂a␈α⊂pacifist␈α∂nor␈α∂a␈α∂non-pacifist.␈α⊂ Combining␈α∂these␈α∂conclusions␈α∂with␈α⊂the␈α∂original

␈↓ α∧␈↓premiss leads to a contradiction.

␈↓ α∧␈↓We use

␈↓ α∧␈↓22)␈↓ αt ␈↓↓∀x.quaker x ∧ ¬ab aspect1 x ⊃ pacifist x␈↓,

␈↓ α∧␈↓23)␈↓ αt ␈↓↓∀x.republican x ∧ ¬ab aspect2 x ⊃ ¬ pacifist x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓24)␈↓ αt ␈↓↓quaker Nixon ∧ republican Nixon␈↓.

␈↓ α∧␈↓␈↓ αTWhen␈α∞we␈α∞circumscribe␈α∂␈↓↓ab z␈↓␈α∞using␈α∞these␈α∞three␈α∂sentences␈α∞as␈α∞␈↓↓A(ab),␈↓␈α∞we␈α∂will␈α∞only␈α∞be␈α∂able␈α∞to

␈↓ α∧␈↓conclude␈αthat␈αNixon␈αis␈α
either␈αabnormal␈αin␈α␈↓↓aspect1␈↓␈α
or␈αin␈α␈↓↓aspect2,␈↓␈αand␈αwe␈α
will␈αnot␈αbe␈αable␈α
to␈αsay

␈↓ α∧␈↓whether␈α∂he␈α∂is␈α∂a␈α∂pacifist.␈α⊂ Of␈α∂course,␈α∂this␈α∂is␈α∂the␈α⊂same␈α∂conclusion␈α∂as␈α∂would␈α∂be␈α⊂reached␈α∂without

␈↓ α∧␈↓circumscription.  The point is merely that we avoid contradiction.

␈↓ α∧␈↓␈↓ αTReiter's␈αsecond␈αexample␈αis␈αthat␈αa␈αperson␈αnormally␈αlives␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈α
and␈αin

␈↓ α∧␈↓the␈αsame␈αcity␈αas␈αhis␈αemployer.␈α But␈αA's␈αwife␈αlives␈αin␈αVancouver␈αand␈αA's␈αemployer␈αis␈αin␈αToronto.

␈↓ α∧␈↓We write

␈↓ α∧␈↓25)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ city x = city wife x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓26)␈↓ αt ␈↓↓∀x.¬ab aspect2 x ⊃ city x = city employer x␈↓.

␈↓ α∧␈↓If we have
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f15


␈↓ α∧␈↓27)␈↓ αt ␈↓↓city wife A = Vancouver ∧ city employer A = Toronto ∧ Toronto ≠ Vancouver␈↓,

␈↓ α∧␈↓we␈α∂will␈α∂again␈α∂only␈α∂be␈α∂able␈α∂to␈α∂conclude␈α⊂that␈α∂A␈α∂lives␈α∂either␈α∂in␈α∂Toronto␈α∂or␈α∂Vancouver.␈α⊂ In␈α∂this

␈↓ α∧␈↓circumscription,␈α
the␈α
function␈α
␈↓↓city␈↓␈α
must␈α
be␈α
taken␈α
as␈α
variable.␈α
 This␈α
might␈α
be␈α
considered␈α
not␈α
entirely

␈↓ α∧␈↓satisfactory.␈α If␈αone␈αknows␈αthat␈αa␈αperson␈αeither␈αdoesn't␈αlive␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈αor␈αdoesn't

␈↓ α∧␈↓live␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αemployer,␈αthen␈α
there␈αis␈αan␈αincreased␈αprobability␈αthat␈αhe␈αdoesn't␈αlive␈α
in

␈↓ α∧␈↓the␈αsame␈αcity␈αas␈αeither.␈α A␈αsystem␈αthat␈αdid␈αreasoning␈αof␈αthis␈αkind␈αwould␈αseem␈αto␈αrequire␈αa␈αlarger

␈↓ α∧␈↓body␈αof␈α
facts␈αand␈αperhaps␈α
more␈αexplicitly␈α
metamathematical␈αreasoning.␈α Not␈α
knowing␈αhow␈α
to␈αdo

␈↓ α∧␈↓that,␈α⊂we␈α⊃might␈α⊂want␈α⊃to␈α⊂use␈α⊃␈↓↓aspect1 x␈↓␈α⊂in␈α⊃both␈α⊂(25)␈α⊃and␈α⊂(26).␈α⊃ Then␈α⊂once␈α⊃we␈α⊂know␈α⊃we␈α⊂would

␈↓ α∧␈↓conclude nothing about his city once we knew that he wasn't in the same city as either.



␈↓ α∧␈↓8. ␈↓αA More general treatment of an ␈↓↓is-a␈↓ hierarchy

␈↓ α∧␈↓␈↓ αTThe␈α∞bird␈α∞example␈α∞works␈α∞fine␈α∞when␈α∞a␈α∞fixed␈α∞␈↓↓is-a␈↓␈α∞hierarchy␈α∞is␈α∞in␈α∞question.␈α∞ However,␈α
our

␈↓ α∧␈↓writing␈αthe␈αinheritance␈αcancellation␈αaxioms␈αdepended␈αon␈αknowing␈αexactly␈αfrom␈αwhat␈αhigher␈αlevel

␈↓ α∧␈↓the␈α∪properties␈α∩were␈α∪inherited.␈α∩ This␈α∪doesn't␈α∩correspond␈α∪to␈α∩my␈α∪intuition␈α∩of␈α∪how␈α∪we␈α∩humans

␈↓ α∧␈↓represent␈α∩inheritance.␈α∩ It␈α∩would␈α∪seem␈α∩rather␈α∩that␈α∩when␈α∩we␈α∪say␈α∩that␈α∩birds␈α∩can␈α∩fly,␈α∪we␈α∩don't

␈↓ α∧␈↓necessarily␈α∞have␈α∞in␈α∞mind␈α∞that␈α
an␈α∞inheritance␈α∞of␈α∞inability␈α∞to␈α
fly␈α∞from␈α∞things␈α∞in␈α∞general␈α∞is␈α
being

␈↓ α∧␈↓cancelled.␈α
 We␈α
can␈α
formulate␈α
inheritance␈α
of␈α
properties␈α
in␈α
a␈α
more␈α
general␈α
way␈α
provided␈α
we␈αreify

␈↓ α∧␈↓the properties.  Presumably there are many ways of doing this, but here's one that seems to work.

␈↓ α∧␈↓␈↓ αTThe␈α∂first␈α∂order␈α∂variables␈α∂of␈α∂our␈α∂theory␈α∂range␈α∂over␈α∂classes␈α∂of␈α∂objects␈α∂(denoted␈α∂by␈α∂␈↓↓c␈↓␈α∞with

␈↓ α∧␈↓numerical␈α
suffixes),␈αproperties␈α
(denoted␈αby␈α
␈↓↓p)␈↓␈α
and␈αobjects␈α
(denoted␈αby␈α
␈↓↓x).␈↓␈αWe␈α
don't␈α
identify␈αour

␈↓ α∧␈↓classes␈α⊗with␈α∃sets␈α⊗(or␈α⊗with␈α∃the␈α⊗classes␈α∃of␈α⊗GB␈α⊗set␈α∃theory).␈α⊗ In␈α∃particular,␈α⊗we␈α⊗don't␈α∃assume

␈↓ α∧␈↓extensionality.  We have several predicates:

␈↓ α∧␈↓␈↓ αT␈↓↓ordinarily(c,p)␈↓␈αmeans␈αthat␈αobjects␈αof␈αclass␈α␈↓↓c␈↓␈αordinarily␈αhave␈αproperty␈α␈↓↓p.␈↓␈α␈↓↓c1 ≤ c2␈↓␈αmeans␈αthat

␈↓ α∧␈↓class␈α␈↓↓c1␈↓␈α
ordinarily␈αinherits␈α
from␈αclass␈α
␈↓↓c2.␈↓␈αWe␈α
assume␈αthat␈α
this␈αrelation␈α
is␈αtransitive.␈α ␈↓↓in(x,c)␈↓␈α
means

␈↓ α∧␈↓that the object ␈↓↓x␈↓ is in class ␈↓↓c.␈↓ ␈↓↓ap(p,x)␈↓ means that property ␈↓↓p␈↓ applies to object ␈↓↓x.␈↓ Our axioms are
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f16


␈↓ α∧␈↓28)␈↓ αt ␈↓↓∀c1 c2 c3. c1 ≤ c2 ∧ c2 ≤ c3 ⊃ c1 ≤ c3␈↓,

␈↓ α∧␈↓29)␈↓ αt ␈↓↓∀c1 c2 p.ordinarily(c2,p) ∧ c1 ≤ c2 ∧ ¬ab aspect1(c1,c2,p) ⊃ ordinarily(c1,p)␈↓,

␈↓ α∧␈↓30)␈↓ αt ␈↓↓∀c1 c2 c3 p.c1 ≤ c2 ∧ c2 ≤ c3 ∧ ordinarily(c2, not p) ⊃ ab aspect1(c1,c3,p)␈↓,

␈↓ α∧␈↓31)␈↓ αt ␈↓↓∀x c p.in(x,c) ∧ ordinarily(c,p) ∧ ¬ab aspect3(x,c,p) ⊃ ap(p,x)␈↓,

␈↓ α∧␈↓32)␈↓ αt ␈↓↓∀x c1 c2 p.in(x,c1) ∧ c1 ≤ c2 ∧ ordinarily(c1,not p) ⊃ ab aspect3(x,c2,p)␈↓.

␈↓ α∧␈↓(28)␈α
is␈α
the␈α
afore-mentioned␈α
transitivity␈αof␈α
≤.␈α
 (29)␈α
says␈α
that␈αproperties␈α
that␈α
ordinarily␈α
hold␈α
for␈αa

␈↓ α∧␈↓class␈α⊃are␈α⊃inherited␈α∩unless␈α⊃something␈α⊃is␈α∩abnormal.␈α⊃ (30)␈α⊃cancels␈α⊃the␈α∩inheritance␈α⊃if␈α⊃there␈α∩is␈α⊃an

␈↓ α∧␈↓intermediate␈αclass␈αfor␈αwhich␈αthe␈αproperty␈αordinarily␈αdoesn't␈αhold.␈α (31)␈αsays␈αthat␈αproperties␈αwhich

␈↓ α∧␈↓ordinarily␈αhold␈αactually␈αhold␈αfor␈αelements␈αof␈αthe␈αclass␈αunless␈αsomething␈αis␈αabnormal.␈α (32)␈αcancels

␈↓ α∧␈↓the␈α⊂effect␈α⊂of␈α⊂(31)␈α⊂when␈α∂there␈α⊂is␈α⊂an␈α⊂intermediate␈α⊂class␈α∂for␈α⊂which␈α⊂the␈α⊂negation␈α⊂of␈α⊂the␈α∂property

␈↓ α∧␈↓ordinarily␈α⊂holds.␈α⊃ Notice␈α⊂that␈α⊃this␈α⊂reification␈α⊂of␈α⊃properties␈α⊂seems␈α⊃to␈α⊂require␈α⊃imitation␈α⊂boolean

␈↓ α∧␈↓operators.  Such operators are discussed in (McCarthy 1979).



␈↓ α∧␈↓9. ␈↓αThe blocks world␈↓

␈↓ α∧␈↓␈↓ αTThe␈α
following␈α
set␈α
of␈α"situation␈α
calculus"␈α
axioms␈α
solves␈α
the␈αframe␈α
problem␈α
for␈α
a␈αblocks␈α
world

␈↓ α∧␈↓in␈α∂which␈α∞blocks␈α∂can␈α∞be␈α∂moved␈α∞and␈α∂painted.␈α∞ Here␈α∂␈↓↓result(e,s)␈↓␈α∞denotes␈α∂the␈α∞situation␈α∂that␈α∞results

␈↓ α∧␈↓when␈α
event␈α␈↓↓e␈↓␈α
occurs␈αin␈α
situation␈α␈↓↓s.␈↓␈α
The␈αformalism␈α
is␈αapproximately␈α
that␈αof␈α
(McCarthy␈αand␈α
Hayes

␈↓ α∧␈↓1969).

␈↓ α∧␈↓33)␈↓ αt ␈↓↓∀x e s.¬ab aspect1(x,e,s) ⊃ location(x,result(e,s)) = location(x,s)␈↓.

␈↓ α∧␈↓34)␈↓ αt ␈↓↓∀x e s.¬ab aspect2(x,e,s) ⊃ color(x,result(e,s)) = color(x,s)␈↓.

␈↓ α∧␈↓Objects change their locations and colors only for a reason.

␈↓ α∧␈↓35)␈↓ αt ␈↓↓∀x l s.ab aspect1(x,move(x,l),s)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x l s.¬ab aspect3(x,l,s) ⊃ location(x,result(move(x,l),s)) = l␈↓.

␈↓ α∧␈↓36)␈↓ αt ␈↓↓∀x c s.ab aspect2(x,paint(x,c),s)␈↓
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f17


␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x c s.¬ab aspect4(x,c,s) ⊃ color(x,result(paint(x,c),s)) = c␈↓.

␈↓ α∧␈↓Objects change their locations when moved and their colors when painted.

␈↓ α∧␈↓37)␈↓ αt ␈↓↓∀x l s.¬clear(top x,s) ∨ ¬clear(l,s) ∨ tooheavy x ∨ l = top x ⊃ ab aspect3(x,move(x,l),s)␈↓.

␈↓ α∧␈↓This␈αprevents␈αthe␈αrule␈α(35)␈αfrom␈αbeing␈αused␈αto␈αinfer␈αthat␈αan␈αobject␈αwill␈αmove␈αif␈αit␈αisn't␈αclear␈αor␈α
to

␈↓ α∧␈↓a␈αdestination␈αthat␈αisn't␈αclear␈αor␈αif␈αthe␈αobject␈αis␈αtoo␈αheavy.␈α An␈αobject␈αalso␈αcannot␈αbe␈αmoved␈αto␈αits

␈↓ α∧␈↓own top.

␈↓ α∧␈↓38)␈↓ αt ␈↓↓∀l s.clear(l,s) ≡ ¬∃x.(¬trivial x ∧ location(x,s) = l)␈↓.

␈↓ α∧␈↓A location is clear if all the objects there are trivial, e.g. a speck of dust.

␈↓ α∧␈↓39)␈↓ αt ␈↓↓∀x.¬ab aspect7 x ⊃ ¬trivial x␈↓.

␈↓ α∧␈↓Trivial objects are abnormal in ␈↓↓aspect7␈↓.



␈↓ α∧␈↓10. ␈↓αAn example of doing the circumscription.␈↓

␈↓ α∧␈↓␈↓ αTIn␈αorder␈αto␈αkeep␈αthe␈α
example␈αshort␈αwe␈αwill␈αtake␈α
into␈αaccount␈αonly␈αthe␈αfollowing␈α
facts␈αfrom

␈↓ α∧␈↓the earlier section on flying.

␈↓ α∧␈↓2) ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓3) ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓4) ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓5) ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓7) ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓␈↓ αTTheir␈α
conjunction␈α
is␈α
taken␈α
as␈α
␈↓↓A(ab,flies)␈↓.␈α This␈α
means␈α
that␈α
what␈α
entities␈α
satisfy␈α
␈↓↓ab␈↓␈αand␈α
what

␈↓ α∧␈↓entities␈α⊃satisfy␈α⊃␈↓↓flies␈↓␈α⊃are␈α⊃to␈α⊃be␈α⊃verified␈α⊃so␈α⊃as␈α⊃to␈α⊃minimize␈α⊃␈↓↓ab z.␈↓␈α⊃Which␈α⊃objects␈α⊃are␈α∩birds␈α⊃and

␈↓ α∧␈↓ostriches are parameters rather than variables, i.e.  what objects are birds is considered given.

␈↓ α∧␈↓␈↓ αTWe␈α
also␈αneed␈α
an␈αaxiom␈α
that␈α
asserts␈αthat␈α
the␈αaspects␈α
are␈α
different.␈α Here␈α
is␈αa␈α
straightforward

␈↓ α∧␈↓version that would be rather long were there more than three aspects.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f18


␈↓ α∧␈↓␈↓↓(∀x y.¬(aspect1 x = aspect2 y))

␈↓ α∧␈↓↓∧ (∀x y.¬(aspect1 x = aspect3 y))

␈↓ α∧␈↓↓∧ (∀x y.¬(aspect2 x = aspect3 y))

␈↓ α∧␈↓↓∧ (∀x y.aspect1 x = aspect1 y ≡ x =y)

␈↓ α∧␈↓↓∧ (∀x y.aspect2 x = aspect2 y ≡ x =y)

␈↓ α∧␈↓↓∧ (∀x y.aspect3 x = aspect3 y ≡ x =y).␈↓

␈↓ α∧␈↓The circumscription formula ␈↓↓A'(ab,flies)␈↓ is then

␈↓ α∧␈↓40)␈↓ αt ␈↓↓A(ab,flies) ∧ ∀ab' flies'.[A(ab',flies') ∧ [∀x. ab' x ⊃ ab x] ⊃ [∀x. ab x ≡ ab' x]]␈↓,

␈↓ α∧␈↓which spelled out becomes

␈↓ α∧␈↓41)␈↓ αt␈α␈↓↓[∀x.¬ab␈α
aspect1␈αx␈α
⊃␈α¬flies␈αx]␈α
∧␈α[∀x.bird␈α
x␈α⊃␈α
ab␈αaspect1␈αx]␈α
∧␈α[∀x.bird␈α
x␈α∧␈α
¬ab␈αaspect2␈αx␈α
⊃

␈↓ α∧␈↓↓flies␈α⊃x]␈α⊃∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃⊃␈α⊃ab␈α⊃aspect2␈α⊃x]␈α∩∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃∧␈α⊃¬ab␈α⊃aspect3␈α⊃x␈α⊃⊃␈α⊃¬flies␈α⊃x]␈α∩∧␈α⊃∀ab'

␈↓ α∧␈↓↓flies'.[[∀x.¬ab'␈αaspect1␈αx␈α⊃␈α¬flies'␈αx]␈α∧␈α[∀x.bird␈αx␈α⊃␈αab'␈αaspect1␈αx]␈α∧␈α[∀x.bird␈αx␈α∧␈α¬ab'␈αaspect2␈αx

␈↓ α∧␈↓↓⊃␈α
flies'␈α
x]␈α
∧␈α
[∀x.ostrich␈αx␈α
⊃␈α
ab'␈α
aspect2␈α
x]␈α∧␈α
[∀x.ostrich␈α
x␈α
∧␈α
¬ab'␈α
aspect3␈αx␈α
⊃␈α
¬flies'␈α
x]␈α
∧␈α[∀z.ab'␈α
z

␈↓ α∧␈↓↓⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓A(ab,flies)␈↓␈α
is␈α
guaranteed␈α
to␈α
be␈α
true,␈α
because␈α
it␈α
is␈α
part␈α
of␈α
what␈α
is␈α
assumed␈α
in␈α
our␈αcommon

␈↓ α∧␈↓sense data base.  Therefore (41) reduces to

␈↓ α∧␈↓42)␈↓ αt␈↓↓∀ab'␈αflies'.[[∀x.¬ab'␈αaspect1␈α
x␈α⊃␈α¬flies'␈α
x]␈α∧␈α[∀x.bird␈αx␈α
⊃␈αab'␈αaspect1␈α
x]␈α∧␈α[∀x.bird␈α
x␈α∧

␈↓ α∧␈↓↓¬ab'␈α∂aspect2␈α∞x␈α∂⊃␈α∞flies'␈α∂x]␈α∞∧␈α∂[∀x.ostrich␈α∞x␈α∂⊃␈α∞ab'␈α∂aspect2␈α∞x]␈α∂∧␈α∞[∀x.ostrich␈α∂x␈α∞∧␈α∂¬ab'␈α∞aspect3␈α∂x␈α∞⊃

␈↓ α∧␈↓↓¬flies' x] ∧ [∀z.ab' z ⊃ ab z] ⊃ [∀z.ab z ≡ ab' z]]␈↓.

␈↓ α∧␈↓␈↓ αTOur␈αobjective␈αis␈αnow␈αto␈αmake␈αsuitable␈αsubstitutions␈αfor␈α␈↓↓ab'␈↓␈αand␈α␈↓↓flies'␈↓␈αso␈αthat␈αall␈α
the␈αterms

␈↓ α∧␈↓preceding␈α∞the␈α∞⊃␈α∞(42)␈α∞will␈α∞be␈α∞true,␈α∂and␈α∞right␈α∞side␈α∞will␈α∞determine␈α∞␈↓↓ab.␈↓␈α∞The␈α∞axiom␈α∂␈↓↓A(ab,flies)␈↓␈α∞will

␈↓ α∧␈↓then␈α
determine␈α∞␈↓↓flies,␈↓␈α
i.e.␈α
we␈α∞will␈α
know␈α
what␈α∞the␈α
fliers␈α
are.␈α∞ ␈↓↓flies'␈↓␈α
is␈α
easy,␈α∞because␈α
we␈α∞need␈α
only

␈↓ α∧␈↓apply␈αwishful␈αthinking;␈αwe␈αwant␈αthe␈αfliers␈αto␈αbe␈αjust␈αthose␈αbirds␈αthat␈αaren't␈αostriches.␈α Therefore,

␈↓ α∧␈↓we put

␈↓ α∧␈↓43)␈↓ αt ␈↓↓flies' x ≡ bird x ∧ ¬ostrich x␈↓.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f19


␈↓ α∧␈↓␈↓ αT␈↓↓ab'␈↓ isn't really much more difficult, but there is a notational problem.  We define

␈↓ α∧␈↓44)␈↓ αt ␈↓↓ab' z ≡ [∃x.bird x ∧ z = aspect1 x] ∨ [∃x.ostrich x ∧ z = aspect2 x]␈↓,

␈↓ α∧␈↓which covers the cases we want to be abnormal.

␈↓ α∧␈↓␈↓ αTAppendix␈α∂A␈α∂contains␈α∂a␈α∞complete␈α∂proof␈α∂as␈α∂accepted␈α∞by␈α∂Jussi␈α∂Ketonen's␈α∂(1984)␈α∞interactive

␈↓ α∧␈↓theorem␈α⊂prover␈α⊂EKL.␈α⊂ EKL␈α⊂uses␈α∂the␈α⊂theory␈α⊂of␈α⊂types␈α⊂and␈α∂therefore␈α⊂has␈α⊂no␈α⊂problem␈α⊂with␈α∂the

␈↓ α∧␈↓second order logic required by circumscription.



␈↓ α∧␈↓11. ␈↓αGeneral considerations and remarks␈↓

␈↓ α∧␈↓␈↓ αT1.␈α
Suppose␈α
we␈α
have␈α
a␈α
data␈α
base␈αof␈α
facts␈α
axiomatized␈α
by␈α
a␈α
formalism␈α
involving␈αthe␈α
predicate

␈↓ α∧␈↓␈↓↓ab.␈↓␈α∩In␈α∩connection␈α∩with␈α∩a␈α∩particular␈α∩problem,␈α∩a␈α∩program␈α∩takes␈α∩a␈α∩subcollection␈α∩of␈α∩these␈α⊃facts

␈↓ α∧␈↓together␈α
with␈α
the␈αspecific␈α
facts␈α
of␈αthe␈α
problem␈α
and␈αthen␈α
circumscribes␈α
␈↓↓ab z.␈↓␈αWe␈α
get␈α
a␈αsecond␈α
order

␈↓ α∧␈↓formula,␈αand␈αin␈αgeneral,␈αas␈αthe␈αnatural␈αnumber␈αexample␈αof␈α(McCarthy␈α1980)␈αshows,␈αthis␈αformula

␈↓ α∧␈↓is␈α∀not␈α∀equivalent␈α∀to␈α∃any␈α∀first␈α∀order␈α∀formula.␈α∃ However,␈α∀many␈α∀common␈α∀sense␈α∃domains␈α∀are

␈↓ α∧␈↓axiomatizable␈αin␈α
such␈αa␈α
way␈αthat␈αthe␈α
circumscription␈αis␈α
equivalent␈αto␈αa␈α
first␈αorder␈α
formula.␈α For

␈↓ α∧␈↓example,␈α
Vladimir␈α
Lifschitz␈α
(unpublished␈α
1983)␈α
has␈α
shown␈α
that␈α
this␈α
is␈α
true␈α
if␈α
the␈α
axioms␈α∞are␈α
a

␈↓ α∧␈↓universal␈α
formula␈αand␈α
there␈αare␈α
no␈α
functions.␈α This␈α
can␈αpresumably␈α
be␈α
extended␈αto␈α
the␈αcase␈α
when

␈↓ α∧␈↓the␈α∞ranges␈α∞and␈α∞domains␈α∞of␈α
the␈α∞functions␈α∞are␈α∞disjoint,␈α∞so␈α∞that␈α
there␈α∞is␈α∞no␈α∞way␈α∞of␈α∞generating␈α
an

␈↓ α∧␈↓infinity of elements.

␈↓ α∧␈↓␈↓ αTWe␈α⊃can␈α⊃then␈α⊃regard␈α⊃the␈α⊃process␈α⊃of␈α⊃deciding␈α⊃what␈α⊃facts␈α⊃to␈α⊃take␈α⊃into␈α⊃account␈α⊃and␈α⊂then

␈↓ α∧␈↓circumscribing␈α
as␈α
a␈αprocess␈α
of␈α
compiling␈αfrom␈α
a␈α
slightly␈αhigher␈α
level␈α
non-monotonic␈αlanguage␈α
into

␈↓ α∧␈↓mathematical␈α∞logic,␈α∂especially␈α∞first␈α∂order␈α∞logic.␈α∂ We␈α∞can␈α∂also␈α∞regard␈α∂natural␈α∞language␈α∂as␈α∞higher

␈↓ α∧␈↓level␈α∀than␈α∀logic.␈α∀ However,␈α∀as␈α∀I␈α∀shall␈α∀discuss␈α∀elsewhere,␈α∀natural␈α∀language␈α∀doesn't␈α∃have␈α∀an

␈↓ α∧␈↓independent␈α∪reasoning␈α∪process,␈α∪because␈α∪most␈α∪natural␈α∪language␈α∪inferences␈α∀involve␈α∪suppressed

␈↓ α∧␈↓premisses␈α∞which␈α∞are␈α∞not␈α∂represented␈α∞in␈α∞natural␈α∞language␈α∞in␈α∂the␈α∞minds␈α∞of␈α∞the␈α∞people␈α∂doing␈α∞the

␈↓ α∧␈↓reasoning.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f20


␈↓ α∧␈↓␈↓ αTReiter␈αhas␈αpointed␈αout,␈αboth␈αinformally␈αand␈αimplicitly␈αin␈α(Reiter␈α1982)␈αthat␈αcircumscription

␈↓ α∧␈↓often␈α∂translates␈α⊂directly␈α∂into␈α⊂Prolog␈α∂program␈α∂once␈α⊂it␈α∂has␈α⊂been␈α∂decided␈α∂what␈α⊂facts␈α∂to␈α⊂take␈α∂into

␈↓ α∧␈↓account.

␈↓ α∧␈↓␈↓ αT2.␈α∂Circumscription␈α∂has␈α∞interesting␈α∂relations␈α∂to␈α∞Reiter's␈α∂(1980)␈α∂logic␈α∞of␈α∂defaults.␈α∂ In␈α∞simple

␈↓ α∧␈↓cases␈αthey␈αgive␈α
the␈αsame␈αresults.␈α However,␈α
a␈αcomputer␈αprogram␈αusing␈α
default␈αlogic␈αwould␈αhave␈α
to

␈↓ α∧␈↓establish␈α∞the␈α∞existence␈α∞of␈α∂models,␈α∞perhaps␈α∞by␈α∞constructing␈α∞them,␈α∂in␈α∞order␈α∞to␈α∞determine␈α∂that␈α∞the

␈↓ α∧␈↓sentences␈α∞mentioned␈α∞in␈α∞default␈α
rules␈α∞were␈α∞consistent.␈α∞ Such␈α
computations␈α∞are␈α∞not␈α∞just␈α
selectively

␈↓ α∧␈↓applying␈α⊂the␈α⊂rules␈α⊃of␈α⊂inference␈α⊂of␈α⊃logic␈α⊂but␈α⊂are␈α⊂metamathematical.␈α⊃ At␈α⊂present␈α⊂this␈α⊃is␈α⊂treated

␈↓ α∧␈↓entirely␈α∞informally,␈α∞and␈α∂I␈α∞am␈α∞not␈α∂aware␈α∞of␈α∞any␈α∂computer␈α∞program␈α∞that␈α∂finds␈α∞models␈α∞of␈α∂sets␈α∞of

␈↓ α∧␈↓sentences or even interacts with a user to find and verify such models.

␈↓ α∧␈↓␈↓ αTCircumscription␈αworks␈α
entirely␈αwithin␈α
the␈αlogic␈α
as␈αAppendices␈α
A␈αand␈α
B␈αillustrate.␈α
 It␈αcan␈α
do

␈↓ α∧␈↓this,␈αbecause␈αit␈αuses␈αsecond␈αorder␈αlogic␈αto␈αimport␈αsome␈αof␈αthe␈αmodel␈αtheory␈αof␈αfirst␈αorder␈αformulas

␈↓ α∧␈↓into␈αthe␈αtheory␈αitself.␈α Finding␈αthe␈αright␈αsubstitution␈αfor␈αthe␈αpredicate␈αvariables␈αis,␈αin␈αthe␈αcases␈αwe

␈↓ α∧␈↓have␈αexamined,␈αthe␈αsame␈αtask␈αas␈αfinding␈αmodels␈αof␈αa␈αfirst␈αorder␈αtheory.␈α Putting␈α
everything␈αinto

␈↓ α∧␈↓the␈α∂logic␈α⊂itself␈α∂is␈α∂an␈α⊂advantage␈α∂as␈α∂long␈α⊂as␈α∂there␈α∂is␈α⊂neither␈α∂a␈α∂good␈α⊂theory␈α∂of␈α∂how␈α⊂to␈α∂construct

␈↓ α∧␈↓models nor programs that do it.

␈↓ α∧␈↓␈↓ αTNotice,␈α∂however,␈α∂that␈α∂finding␈α∂an␈α∂interpretation␈α∂of␈α∂a␈α∂language␈α∂has␈α∂two␈α∂parts␈α∂-␈α∂finding␈α∂a

␈↓ α∧␈↓domain␈α∂and␈α∂interpreting␈α∂the␈α∂predicate␈α∂and␈α∂function␈α∂letters␈α∂by␈α∂predicates␈α∂and␈α∂functions␈α⊂on␈α∂the

␈↓ α∧␈↓domain.␈α It␈αseems␈αthat␈αthe␈αsecond␈αis␈αeasier␈αto␈αimport␈αinto␈αsecond␈αorder␈αlogic␈αthan␈αthe␈α
first.␈α This

␈↓ α∧␈↓may be why our treatment of unique names is awkward.

␈↓ α∧␈↓␈↓ αT3.␈α
The␈α∞axioms␈α
introduced␈α
in␈α∞this␈α
paper␈α
are␈α∞still␈α
not␈α
in␈α∞a␈α
suitable␈α
form␈α∞for␈α
inclusion␈α∞in␈α
a

␈↓ α∧␈↓common␈αsense␈αdatabase.␈α Some␈αof␈αthe␈αcircumscriptions␈αhave␈αunwanted␈αconclusions,␈αe.g.␈αthat␈αthere

␈↓ α∧␈↓are␈α∀no␈α∀ostriches␈α∪if␈α∀none␈α∀are␈α∀explicitly␈α∪mentioned.␈α∀ Perhaps␈α∀some␈α∀of␈α∪this␈α∀can␈α∀be␈α∀fixed␈α∪by

␈↓ α∧␈↓introducing␈α
the␈α
notion␈α
of␈α
present␈α
situation.␈α
 An␈α
axiom␈α
that␈α
ostriches␈α
exist␈α
will␈α
do␈α
no␈α
harm␈αif␈α
what

␈↓ α∧␈↓is allowed to vary includes only ostriches that are present.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f21


␈↓ α∧␈↓␈↓ αT4.␈α∂We␈α⊂are␈α∂only␈α⊂part␈α∂way␈α∂to␈α⊂our␈α∂goal␈α⊂of␈α∂providing␈α∂a␈α⊂formalism␈α∂in␈α⊂which␈α∂a␈α⊂database␈α∂of

␈↓ α∧␈↓common␈α
sense␈α
knowledge␈α
can␈αbe␈α
expressed.␈α
 Besides␈α
sets␈α
of␈αaxioms␈α
involving␈α
␈↓↓ab,␈↓␈α
we␈α
need␈αways␈α
of

␈↓ α∧␈↓specifying␈α∂what␈α∂facts␈α∂shall␈α∂be␈α∂taken␈α∂into␈α∞account␈α∂and␈α∂what␈α∂functions␈α∂and␈α∂predicates␈α∂are␈α∂to␈α∞be

␈↓ α∧␈↓taken as variable.



␈↓ α∧␈↓␈↓αAppendix A␈↓

␈↓ α∧␈↓Circumscription in a Proof Checker

␈↓ α∧␈↓␈↓ αTEKL␈αis␈αan␈αinteractive␈αproof␈αchecker␈α
for␈αthe␈αtheory␈αof␈αtypes.␈α The␈αpresent␈α
argument␈αmakes

␈↓ α∧␈↓use␈αof␈α
its␈αability␈α
to␈αdo␈α
second␈αorder␈α
logic.␈α Each␈αstep␈α
begins␈αwith␈α
a␈αcommand␈α
given␈αby␈α
the␈αuser.

␈↓ α∧␈↓This␈αis␈αusually␈αfollowed␈αby␈αthe␈αsentence␈αresulting␈αfrom␈αthe␈αstep,␈αbut␈αthis␈αis␈αomitted␈αfor␈α
definitions

␈↓ α∧␈↓when the information is contained in the command.  We follow each step by a brief explanation.

␈↓ α∧␈↓ε1. (DEFINE A
␈↓ α∧␈↓ε     |∀AB FLIES.A(AB,FLIES)≡
␈↓ α∧␈↓ε                (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε                (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧
␈↓ α∧␈↓ε                (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε                (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)
␈↓ α∧␈↓εThis defines the second order predicate ␈↓↓A(ab,flies)␈↓ε, where ␈↓↓ab␈↓ε and
␈↓ α∧␈↓ε␈↓↓flies␈↓ε are predicate variables.  Included here are the specific facts
␈↓ α∧␈↓εabout flying being taken into account.

␈↓ α∧␈↓ε;labels: SIMPINFO
␈↓ α∧␈↓ε2. (AXIOM
␈↓ α∧␈↓ε    |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
␈↓ α∧␈↓ε     (∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
␈↓ α∧␈↓ε     (∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)
␈↓ α∧␈↓εThese facts about the distinctness of aspects are used in step 26 only.
␈↓ α∧␈↓εSince axiom 2 is labelled SIMPINFO, the EKL simplifier uses it
␈↓ α∧␈↓εwhen appropriate when it is asked to simplify a formula.

␈↓ α∧␈↓ε3. (DEFINE A1
␈↓ α∧␈↓ε     |∀AB FLIES.A1(AB,FLIES)≡
␈↓ α∧␈↓ε                A(AB,FLIES)∧
␈↓ α∧␈↓ε                (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|
␈↓ α∧␈↓ε     NIL)
␈↓ α∧␈↓εThis is the circumscription formula itself.

␈↓ α∧␈↓ε4. (ASSUME |A1(AB,FLIES)|)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εSince EKL cannot be asked (yet) to do a circumscription, we assume the
␈↓ α∧␈↓εresult.  Most subsequent statements list line 4 as a dependency.
␈↓ α∧␈↓εThis is appropriate since circumscription is a rule of conjecture rather
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f22


␈↓ α∧␈↓εthan a rule of inference.

␈↓ α∧␈↓ε5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)
␈↓ α∧␈↓εThis definition and the next say what we are going to substitute for
␈↓ α∧␈↓εthe bound predicate variables.

␈↓ α∧␈↓ε6. (DEFINE AB2
␈↓ α∧␈↓ε     |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))|
␈↓ α∧␈↓εNIL)
␈↓ α∧␈↓εThe fact that this definition is necessarily somewhat awkward makes
␈↓ α∧␈↓εfor some difficulty throughout the proof.

␈↓ α∧␈↓ε7. (RW 4 (OPEN A1))
␈↓ α∧␈↓εA(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εThis step merely expands out the circumscription formula.

␈↓ α∧␈↓ε8. (TRW |A(AB,FLIES)| (USE 7))
␈↓ α∧␈↓εA(AB,FLIES)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εWe separate the two conjuncts of 7 in this and the next step.

␈↓ α∧␈↓ε9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))|
␈↓ α∧␈↓ε(USE 7))
␈↓ α∧␈↓ε∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
␈↓ α∧␈↓εdeps: (4)

␈↓ α∧␈↓ε10. (RW 8 (OPEN A))
␈↓ α∧␈↓ε(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
␈↓ α∧␈↓ε(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εExpanding out the axiom using the definition ␈↓↓a␈↓ε in step 1.

␈↓ α∧␈↓ε11. (ASSUME |AB2(Z)|)
␈↓ α∧␈↓εdeps: (11)
␈↓ α∧␈↓εOur goal is step 15, but we need to assume its premiss and then
␈↓ α∧␈↓εderive its conclusion.

␈↓ α∧␈↓ε12. (RW 11 (OPEN AB2))
␈↓ α∧␈↓ε(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
␈↓ α∧␈↓εdeps: (11)
␈↓ α∧␈↓εWe use the definition of ␈↓↓ab2␈↓ε.

␈↓ α∧␈↓ε13. (DERIVE |AB(Z)| (12 10) NIL)
␈↓ α∧␈↓εAB(Z)
␈↓ α∧␈↓εdeps: (4 11)
␈↓ α∧␈↓εHere EKL did a lot of work using its DERIVE command.  It took about
␈↓ α∧␈↓εten seconds of computer time on this step.

␈↓ α∧␈↓ε14. (CI (11) 13 NIL)
␈↓ α∧␈↓εAB2(Z)⊃AB(Z)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εWe discharge the assumption 11.

␈↓ α∧␈↓ε15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f23


␈↓ α∧␈↓ε∀Z.AB2(Z)⊃AB(Z)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εUniversal generalization.

␈↓ α∧␈↓ε16. (DERIVE |∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)
␈↓ α∧␈↓εWe need to show that ␈↓↓ab2␈↓ε satisfies the axiom defining ␈↓↓ab.␈↓ε  This
␈↓ α∧␈↓εtakes till step 22, because we have to do the parts separately if
␈↓ α∧␈↓εwe want DERIVE to do the work for us.

␈↓ α∧␈↓ε17. (DERIVE |∀X.BIRD(X)⊃AB2(ASPECT1(X))| (5 6) NIL)
␈↓ α∧␈↓ε∀X.BIRD(X)⊃AB2(ASPECT1(X))

␈↓ α∧␈↓ε18. (DERIVE |∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)

␈↓ α∧␈↓ε19. (DERIVE |∀X.OSTRICH(X)⊃AB2(ASPECT2(X))| (5 6) NIL)
␈↓ α∧␈↓ε∀X.OSTRICH(X)⊃AB2(ASPECT2(X))

␈↓ α∧␈↓ε20. (DERIVE |∀X.OSTRICH(X)⊃¬FLIES2(X)| (5 6) NIL)
␈↓ α∧␈↓ε∀X.OSTRICH(X)⊃¬FLIES2(X)
␈↓ α∧␈↓εOur subgoal was step 21 but DERIVE ran out of push down list when
␈↓ α∧␈↓εwe tried to do it in one step.

␈↓ α∧␈↓ε21. (DERIVE |∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)| (20) NIL)
␈↓ α∧␈↓ε∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)

␈↓ α∧␈↓ε22. (DERIVE
␈↓ α∧␈↓ε      |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε       (∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| (16 17 18 19 20 21)
␈↓ α∧␈↓εNIL)
␈↓ α∧␈↓ε(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓εHere we form a conjunction.

␈↓ α∧␈↓ε23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
␈↓ α∧␈↓εA(AB2,FLIES2)≡
␈↓ α∧␈↓ε(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
␈↓ α∧␈↓ε(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))
␈↓ α∧␈↓εNow we substitute ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε in the definition of ␈↓↓A␈↓ε and get
␈↓ α∧␈↓εa result we can compare with step 22.

␈↓ α∧␈↓ε24. (RW 23 (USE 22))
␈↓ α∧␈↓εA(AB2,FLIES2)
␈↓ α∧␈↓εWe have shown that ␈↓↓ab2␈↓ε and ␈↓↓flies2␈↓ε satisfy ␈↓↓A.␈↓ε

␈↓ α∧␈↓ε25. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 24) NIL)
␈↓ α∧␈↓ε∀Z.AB(Z)≡AB2(Z)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓ε9 was the circumscription formula, and 15 and 24 are its two premisses,
␈↓ α∧␈↓εso we can now derive its conclusion.  Now we know exactly what entities
␈↓ α∧␈↓εare abnormal.
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f24


␈↓ α∧␈↓ε26. (RW 8 ((USE 1 MODE: EXACT) ((USE 25 MODE: EXACT) (OPEN AB2))))
␈↓ α∧␈↓ε(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧
␈↓ α∧␈↓ε(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓εWe rewrite the axiom now that we know what's abnormal.  This gives
␈↓ α∧␈↓εa somewhat awkward formula that nevertheless contains the desired
␈↓ α∧␈↓εconclusion.  The occurrences of equality are left over from the
␈↓ α∧␈↓εelimination of the aspects that used the axiom of step 2.  You should
␈↓ α∧␈↓εsee what step 26 looked like before we got that axiom properly
␈↓ α∧␈↓εformulated.

␈↓ α∧␈↓ε27. (DERIVE |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| (26) NIL)
␈↓ α∧␈↓ε∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)
␈↓ α∧␈↓εdeps: (4)
␈↓ α∧␈↓DERIVE straightens out 26 to put the conclusion in the desired form.
␈↓ α∧␈↓The result is still dependent on the assumption of the correctness of
␈↓ α∧␈↓the circumscription made in step 4.

␈↓ α∧␈↓␈↓ αTClearly if circumscription is to become a practical technique,
␈↓ α∧␈↓the reasoning has to become much more automatic.



␈↓ α∧␈↓␈↓αAppendix B␈↓

␈↓ α∧␈↓␈↓ αTHere␈αis␈αan␈α
annotated␈αEKL␈αproof␈α
that␈αcircumscribes␈αthe␈α
predicate␈α␈↓↓e(x,y)␈↓␈αdiscussed␈αin␈α
section

␈↓ α∧␈↓6.

␈↓ α∧␈↓ε;the proof EQUAL:

␈↓ α∧␈↓ε;This proof uses circumscription to maximize the uniqueness of names, through
␈↓ α∧␈↓ε;the circumscription of an equivalence relation E(X,Y), which is to be
␈↓ α∧␈↓ε;interpreted as asserting the equivalence of the objects denoted by X and Y.

␈↓ α∧␈↓ε;labels: SIMPINFO
␈↓ α∧␈↓ε1. (AXIOM |INDEX(A)=1∧INDEX(B)=2∧INDEX(C)=3∧INDEX(D)=4|)
␈↓ α∧␈↓ε;Since EKL does not have attachments to determine the equivalence of names,
␈↓ α∧␈↓ε;we establish a correspondence between the names in our domain and the integers.
␈↓ α∧␈↓ε;The label SIMPINFO on this statement and the next indicates that these statements
␈↓ α∧␈↓ε;should be used by the EKL simplifier whenever appropriate;

␈↓ α∧␈↓ε;labels: SIMPINFO
␈↓ α∧␈↓ε2. (AXIOM |¬1=2∧¬1=3∧¬2=3∧¬1=4∧¬2=4∧¬2=4|)
␈↓ α∧␈↓ε;Unfortunately, EKL does not have a sufficiently sophisticated number theory
␈↓ α∧␈↓ε;to recognize the uniqueness of integers -- this should not be necessary.

␈↓ α∧␈↓ε3. (DEFINE EQUIV
␈↓ α∧␈↓ε     |∀E.EQUIV(E)≡
␈↓ α∧␈↓ε         (∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))| NIL)
␈↓ α∧␈↓ε;Here we state the conditions necessary for E to be an equivalence relation.
␈↓ α∧␈↓ε;It must be reflexive, symmetric, and transitive.

␈↓ α∧␈↓ε4. (DEFINE WORLD |∀E.WORLD(E)≡E(A,B)∧EQUIV(E)| NIL)
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f25


␈↓ α∧␈↓ε;This axiom describes the world we are considering in this example.  There
␈↓ α∧␈↓ε;is an equivalence relation, E, which holds for two names, A and B.

␈↓ α∧␈↓ε5. (DEFINE WORLD1
␈↓ α∧␈↓ε     |∀E.WORLD1(E)≡
␈↓ α∧␈↓ε         WORLD(E)∧
␈↓ α∧␈↓ε         (∀E1.WORLD(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))| NIL)
␈↓ α∧␈↓ε;This is the circumscription formula -- we are circumscribing the equivalence
␈↓ α∧␈↓ε;relation E.

␈↓ α∧␈↓ε6. (ASSUME |WORLD1(E)|)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Since EKL cannot do the circumscription, we assume the result.  Many subsequent
␈↓ α∧␈↓ε;statements will list 6 as a dependency because of this.

␈↓ α∧␈↓ε7. (DEFINE E2 |∀X Y.E2(X,Y)≡X=A∧Y=B∨X=Y| NIL)
␈↓ α∧␈↓ε;This is what we would like E1 to be in WORLD1.  The only equivalent pairs
␈↓ α∧␈↓ε;are [A,B] and pairs in which both elements are the same.

␈↓ α∧␈↓ε8. (DERIVE |EQUIV(E2)| (NIL) ((OPEN EQUIV) (OPEN E2)))
␈↓ α∧␈↓ε;EQUIV(E2)
␈↓ α∧␈↓ε;We infer that E2 is an equivalence relation.

␈↓ α∧␈↓ε9. (DERIVE |WORLD(E2)| (8) ((OPEN WORLD) (OPEN E2)))
␈↓ α∧␈↓ε;WORLD(E2)
␈↓ α∧␈↓ε;The relation E2 satisfies the definition of WORLD.

␈↓ α∧␈↓ε10. (RW 6 (OPEN WORLD1))
␈↓ α∧␈↓ε;WORLD(E)∧(∀E1.WORLD(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y)))
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Here we expand the circumscription formula.

␈↓ α∧␈↓ε11. (DERIVE |WORLD(E)| (10) NIL)
␈↓ α∧␈↓ε;WORLD(E)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;This is the first conjunct of the previous statement.

␈↓ α∧␈↓ε12. (RW 11 (OPEN WORLD))
␈↓ α∧␈↓ε;E(A,B)∧EQUIV(E)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Expanding the definition of WORLD.

␈↓ α∧␈↓ε13. (RW 12 (OPEN EQUIV))
␈↓ α∧␈↓ε;E(A,B)∧(∀X.E(X,X))∧(∀X Y.E(X,Y)⊃E(Y,X))∧(∀X Y Z.E(X,Y)∧E(Y,Z)⊃E(X,Z))
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Expanding the definition of EQUIV

␈↓ α∧␈↓ε14. (DERIVE |∀X Y.E2(X,Y)⊃E(X,Y)| (12 13) (OPEN E11))
␈↓ α∧␈↓ε;∀X Y.E2(X,Y)⊃E(X,Y)
␈↓ α∧␈↓ε;deps: (6)

␈↓ α∧␈↓ε15. (DERIVE |∀E1.WORLD(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y))|
␈↓ α∧␈↓ε      (10) NIL)
␈↓ α∧␈↓ε;∀E1.WORLD(E1)∧(∀X Y.E1(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E1(X,Y))
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f26


␈↓ α∧␈↓ε16. (UE ((E1.|E2|)) 15 NIL)
␈↓ α∧␈↓ε;WORLD(E2)∧(∀X Y.E2(X,Y)⊃E(X,Y))⊃(∀X Y.E(X,Y)≡E2(X,Y))
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;In the last three steps, we have proven that E2 satisfies the circumscription
␈↓ α∧␈↓ε;formula.

␈↓ α∧␈↓ε17. (DERIVE |∀X Y.E(X,Y)≡E2(X,Y)| (9 14 16) NIL)
␈↓ α∧␈↓ε;∀X Y.E(X,Y)≡E2(X,Y)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Now we can find the set of equivalent pairs.

␈↓ α∧␈↓ε18. (RW 17 (OPEN E2))
␈↓ α∧␈↓ε;∀X Y.E(X,Y)≡X=A∧Y=B∨X=Y
␈↓ α∧␈↓ε;deps: (6)

␈↓ α∧␈↓ε19. (DERIVE |E(A,B)| (18) NIL)
␈↓ α∧␈↓ε;E(A,B)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;As before, A and B are equivalent.

␈↓ α∧␈↓ε20. (DERIVE |¬A=C| (SIMPINFO) NIL)
␈↓ α∧␈↓ε;¬A=C
␈↓ α∧␈↓ε;From the axioms at the beginning, we derive the uniqueness of names.

␈↓ α∧␈↓ε21. (DERIVE |¬B=C| (SIMPINFO) NIL)
␈↓ α∧␈↓ε;¬B=C

␈↓ α∧␈↓ε22. (DERIVE |¬E(A,C)| (18 20 21) NIL)
␈↓ α∧␈↓ε;¬E:A,C)
␈↓ α∧␈↓ε;deps: (6)
␈↓ α∧␈↓ε;Here we demonstrate that things not explicitly stated to be equivalent
␈↓ α∧␈↓ε;in our definition of the world are not equivalent.


␈↓ α∧␈↓12. Acknowledgments

␈↓ α∧␈↓␈↓ αTI␈α
have␈αhad␈α
useful␈αdiscussions␈α
with␈αMatthew␈α
Ginsberg,␈αBenjamin␈α
Grosof,␈αand␈α
Leslie␈αPack.

␈↓ α∧␈↓The work was partially supported by NSF and by DARPA.


␈↓ α∧␈↓13. ␈↓αReferences:␈↓

␈↓ α∧␈↓␈↓αEtherington,␈α→David␈α→W.␈α→and␈α→Raymond␈α→Reiter␈α→(1983)␈↓:␈α→"On␈α→Inheritance␈α~Hierarchies␈α→with
␈↓ α∧␈↓Exceptions",␈α∀in␈α∀␈↓↓Proceedings␈α∀of␈α∀the␈α∀National␈α∀Conference␈α∀on␈α∀Artificial␈α∀Intelligence,␈α∀AAAI-83␈↓,
␈↓ α∧␈↓William Kaufman, Inc.

␈↓ α∧␈↓␈↓αKetonen,␈α⊂Jussi␈α⊃and␈α⊂Joseph␈α⊂S.␈α⊃Weening␈α⊂(1984)␈↓:␈α⊃␈↓↓EKL␈α⊂-␈α⊂An␈α⊃Interactive␈α⊂Proof␈α⊃Checker,␈α⊂User's
␈↓ α∧␈↓↓Reference Manual␈↓, Computer Science Department, Stanford University.

␈↓ α∧␈↓␈↓αLifschitz, Vladimir␈↓(1983): unpublished note on circumscription
␈↓ α∧␈↓␈↓ ¬4Applications of Circumscription␈↓ f27


␈↓ α∧␈↓␈↓αMcCarthy,␈α∂John␈α∂and␈α∞P.J.␈α∂Hayes␈α∂(1969)␈↓:␈α∞"Some␈α∂Philosophical␈α∂Problems␈α∞from␈α∂the␈α∂Standpoint␈α∞of
␈↓ α∧␈↓Artificial␈α
Intelligence",␈α∞in␈α
D.␈α
Michie␈α∞(ed),␈α
␈↓↓Machine␈α
Intelligence␈α∞4␈↓,␈α
American␈α
Elsevier,␈α∞New␈α
York,
␈↓ α∧␈↓NY.

␈↓ α∧␈↓␈↓αMcCarthy,␈α∂John␈α∂(1977)␈↓:␈α∂"Epistemological␈α∂Problems␈α∂of␈α∂Artificial␈α∂Intelligence",␈α∂␈↓↓Proceedings␈α∂of␈α∞the
␈↓ α∧␈↓↓Fifth International Joint Conference on Artificial Intelligence␈↓, M.I.T., Cambridge, Mass.

␈↓ α∧␈↓␈↓αMcCarthy,␈α∪John␈α∩(1979)␈↓:␈α∪"First␈α∩Order␈α∪Theories␈α∩of␈α∪Individual␈α∩Concepts␈α∪and␈α∪Propositions",␈α∩in
␈↓ α∧␈↓Michie, Donald (ed.) ␈↓↓Machine Intelligence 9␈↓, (University of Edinburgh Press, Edinburgh).

␈↓ α∧␈↓␈↓αMcCarthy,␈α⊃John␈α⊃(1980)␈↓:␈α⊃"Circumscription␈α∩-␈α⊃A␈α⊃Form␈α⊃of␈α⊃Non-Monotonic␈α∩Reasoning",␈α⊃␈↓↓Artificial
␈↓ α∧␈↓↓Intelligence␈↓, Volume 13, Numbers 1,2, April.

␈↓ α∧␈↓␈↓αMinsky,␈α
Marvin␈α
(1982)␈↓:␈α
in␈α
various␈α
lectures␈α
including␈α
AAAI␈α
Presidential␈α
Address␈α
though␈α
not␈αin␈α
its
␈↓ α∧␈↓written form.

␈↓ α∧␈↓␈↓αReiter,␈α⊃Raymond␈α⊃(1980)␈↓:␈α⊃"A␈α⊃Logic␈α⊃for␈α⊃Default␈α⊃Reasoning",␈α⊃␈↓↓Artificial␈α⊃Intelligence␈↓,␈α⊃Volume␈α⊂13,
␈↓ α∧␈↓Numbers 1,2, April.

␈↓ α∧␈↓␈↓αReiter,␈α
Raymond␈α∞(1980b)␈↓:␈α
"Equality␈α
and␈α∞domain␈α
closure␈α
in␈α∞first␈α
order␈α
data␈α∞bases",␈α
J.␈α∞ACM,␈α
27,
␈↓ α∧␈↓Apr. 1980, 235-249.

␈↓ α∧␈↓␈↓αReiter,␈α!Raymond␈α!(1982)␈↓:␈α""Circumscription␈α!Implies␈α!Predicate␈α"Completion␈α!(Sometimes)",
␈↓ α∧␈↓Proceedings of the National Conference on Artificial Intelligence, AAAI-82.

␈↓ α∧␈↓This version of circum[f83,jmc] pubbed at 14:26 on May 15, 1984.